Homotopy Type Theory using the Agda HoTT library

Forward

This guide is intended to serve as a walk-through for the book Homotopy Type Theory. It will list and discuss all theorems, definitions and exercises in the programming language Agda using the Homotopy Type Theory (HoTT) library.

One should read this book with Agda and the HoTT library installed on their computers. It serves as a complement to the Homotopy Type Theory book, so you should have a copy in hand as you read this.

This guide will follow the HoTT book closely, with appendices at the end for further explanations of the HoTT library.