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

Type Theory Forall

• Episode: #16 Agda, K Axiom, HoTT, Rewrite Theory - Jesper Cockx
• Website: Type Theory Forall
• Feed URL: https://www.typetheoryforall.com/episodes.mp3.rss
• Duration: 01:36:53
• Published: 2022-04-02 18:20

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

• Jesper’s Website
• Jesper’s Twitter: @agdakx
• Jesper’s PhD Thesis
• Rewrite Theory paper
• Pattern matching without K paper (Check his website for more)
• EuroProofNet
• WITS Talks on Youtube (Workshop on the Implementation of Type Systems)
• Agda Zulip
• Agda Mailing List
• Ataca Github
• Wadler’s book on Agda
• Stump’s book on Agda