Logo

Type Theory Forall

Type Theory much beyond inference rules

Episode image

#16 Agda, K Axiom, HoTT, Rewrite Theory

Jesper Cockx

Apr 11th 2024   |  96 min
0:00
0:00

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