Type Theory Forall

#16 Agda, K Axiom, HoTT, Rewrite Theory - Jesper Cockx

Type Theory Forall

In this episode we interview Jesper Cockx, one of the core developers on Agda. We talk about the philosophy behind Agda, his work on pattern matching, the Uniqueness of Identity of Proofs, UIP for short, and why it is inconsistent with Homotopy Type Theory.

Links

Next Episodes