Homotopy Type Theory

A formalization of the Homotopy Type Theory Book in agda, made by Fernando Chu. The source code can be found at the following github repo.

Part I - Foundations

Chapter 1. Type Theory

open import Chapter1.Book public
open import Chapter1.Exercises public

Chapter 2. Homotopy Type Theory

open import Chapter2.Book public
open import Chapter2.Exercises public

Chapter 3. Sets and Logic

open import Chapter3.Book public
open import Chapter3.Exercises public

Chapter 4. Equivalences

open import Chapter4.Book public
open import Chapter4.Exercises public

Chapter 5. Induction

open import Chapter5.Book public
open import Chapter5.Exercises public

Chapter 6. Higher Inductive Types

open import Chapter6.Book public
open import Chapter6.Exercises public

Chapter 7. Homotopy n-types

open import Chapter7.Book public
open import Chapter7.Exercises public

Part II - Mathematics

Chapter 8. Homotopy Theory

open import Chapter8.Book public
open import Chapter8.Exercises public

Chapter 9. Category Theory

open import Chapter9.Book public
open import Chapter9.Exercises public

Chapter 10. Set Theory

open import Chapter10.Book public
open import Chapter10.Exercises public

Chapter 11. Real Numbers

open import Chapter11.Book public
open import Chapter11.Exercises public

Acknowledgments

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.