Posts tagged with "type-theory"

Reflections on my first type theory talk

Visual examples of hcomp

Boolean equivalences

Path induction: a GADT perspective

Formally proving true ≢ false in Homotopy Type Theory with Agda