Formalization of the HoTT Book in Agda.
A formalization of the Homotopy Type Theory Book in Agda.
The code can be explored in our github page.
I've tried to keep the Agda as simple as possible, while using similar naming conventions to the HoTT book. Some workarounds have to be done sometimes to please agda, I've tried to mention them somehow when the need arises.
Like the book, function extensionality and univalence are assumed, as well as the existence of HITs. Unlike it, I take careful track of the universe indices (mainly to please agda).
A lot of my code is taken from Escardo's notes. Other references I used where agda-unimath, Rijke's formalization of his book, the HoTT-Agda library, and of course Agda's standard library.
The css styles were taken from the HoTTEST summer school repo.
Any contribution, be it in improving the readability of a proof, additional content from the book (I've skipped a ton), or just a simple typo is appreciated.