---
title: Homotopy Type Theory
isIndex: true
---

<!--
```agda
module index where
```
-->

# 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](https://github.com/shiranaiyo/HoTT-Book-Agda).

## Part I - Foundations

### Chapter 1. Type Theory

```agda
open import Chapter1.Book public
open import Chapter1.Exercises public
```

### Chapter 2. Homotopy Type Theory

```agda
open import Chapter2.Book public
open import Chapter2.Exercises public
```

### Chapter 3. Sets and Logic

```agda
open import Chapter3.Book public
open import Chapter3.Exercises public
```

### Chapter 4. Equivalences

```agda
open import Chapter4.Book public
open import Chapter4.Exercises public
```

### Chapter 5. Induction

```agda
open import Chapter5.Book public
open import Chapter5.Exercises public
```

### Chapter 6. Higher Inductive Types

```agda
open import Chapter6.Book public
open import Chapter6.Exercises public
```

### Chapter 7. Homotopy n-types

```agda
open import Chapter7.Book public
open import Chapter7.Exercises public
```

## Part II - Mathematics

### Chapter 8. Homotopy Theory

```agda
open import Chapter8.Book public
open import Chapter8.Exercises public
```

### Chapter 9. Category Theory

```agda
open import Chapter9.Book public
open import Chapter9.Exercises public
```

### Chapter 10. Set Theory

```agda
open import Chapter10.Book public
open import Chapter10.Exercises public
```

### Chapter 11. Real Numbers

```agda
open import Chapter11.Book public
open import Chapter11.Exercises public
```

### Acknowledgments

A lot of my code is taken from Escardo's [notes](https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html).
Other references I used where [agda-unimath](https://unimath.github.io/agda-unimath/), Rijke's [formalization](https://github.com/HoTT-Intro/Agda) of his book, the [HoTT-Agda](https://github.com/HoTT/HoTT-Agda) library, and of course Agda's [standard library](https://github.com/agda/agda-stdlib).

The css styles were taken from the [HoTTEST summer school](https://github.com/martinescardo/HoTTEST-Summer-School) repo.
