HoTT Library

Notes on the HoTT Library

We use this page to help coordinate the work on the HoTT library, including a “wish list” of definitions and theorems we would like to have added to the library.

For the status of the implementation of the HoTT book, please see book.md.

Style

We mostly follow the style guide for the standard library.

Wish list

• For various structures, characterize the equality type in it. So e.g. for pointed maps we want a theorem:

definition pmap_eq_equiv (f g : A →* B) : (f = g) ≃ (f ~* g)

(the maps back and forth have already been defined). Similarly we want to characterize the equality type in pointed types, pointed homotopies, pointed equivalences, and perhaps all of the algebraic hierarchy...

• For various higher inductive types, give the non-dependent and the dependent universal property and the flattening lemma (this is done for some HITs, but not all).
• Show that various constructions (like inverseo) for pathovers (defined in init.pathover are equivalences), similar to the proofs in types.eq for constructions for paths.
• Formalize chapters 10.2, 10.3 and 10.4 about cardinals and ordinals from the book.
• The van Kampen theorem (could port from Agda).
• The 3x3 lemma (could port from Agda).
• The results from section 8.8 of the book, most notably the truncated Whitehead theorem (Theorem 8.8.3)
• Blakers-Massey Theorem (Faviona's Agda formalization is here, Dan Licata has a different formalization)
• add more here