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

• The van Kampen theorem (could port from Agda).
• The 3x3 lemma (could port from Agda).
• add more here