HoTT in Idris

This repository contains some of the content in the Homotopy Type Theory textbook in Idris. Of course, univalence is inconsistent with the brand of pattern-matching that Idris has (which implies the uniqueness of identity proofs, axiom K, etc.), so I have to be careful never to match on Refl. According to Pattern-Matching without K, this is only an issue when pattern-matching on Refl produces a unification problem shaped like x = x, but just to be safe, I use eliminators (i.e. J) throughout instead.

• TypeTheory: Chapter 1
• Homotopy: Chapter 2 - Sections 2.1 to 2.4
• TypeFormers: Chapter 2 - Sections 2.5 to 2.15
• FunExt: Sections 2.9, 4.9, and 6.3 (TODO)
• SetsLogic: Chapter 3
• Equivalence: Second half of Section 2.4; Chapter 4

Program holes

These are places where the type has been declared with no implementation given, or filled in with believe_me.

Axioms

• FunExt.fun_refl

Higher inductive types

• FunExt.Interval: seg, seg_comp
• SetsLogic.Squash: squash

Partially-completed proofs

• Homotopy.EckmannHilton
• TypeFormers.ap_uniq (will not do)
• SetsLogic.ACqinvCP
• SetsLogic.contrFamilyCentre: fg

TODOs

Some of these have been partially begun and show up as program holes in the above.

• Section 2.1: Theorem 2.1.6 (EckmannHilton)
• Sections 2.10, 2.12, 2.13
• Section 3.8: Lemma 3.8.2 (ACqinvCP)
• Section 3.11: Lemma 3.11.9 (ii)/Exercise 3.20 (contrFamilyCentre)
• Section 4.3: Theorem 4.3.2
• Section 4.4: Corollary 4.4.6

These I do not plan on ever doing.

• Section 2.11: Theorems 2.11.3 to 2.11.5
• Section 2.14
• Section 2.15: Equations 2.15.9 to 2.15.11
• Sections 4.1 to 4.2, 4.6, 4.8
• Section 4.7: Theorems 4.7.1 to 4.7.4
• Section 4.9: Definition 4.9.1 to Theorem 4.9.4

Bonus content

• PLFI: Programming Language Foundations in Agda, but in Idris. This only contains some of the sections I find interesting.