General References

Foundational

1. Papers by Per Martin-Löf, mathematician and philosopher.
2. It is impossible to understate the importance of Voevodsky’s ideas.
3. Homotopy theoretic models of identity types by S. Awodey and M. Warren. Also at arXiv.org

Textbooks

1. The Symmetry Book: a work in progress under the UniMath umbrella. In their own words:

   […] an undergraduate textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.

2. Our reference text, the Homotopy Type Theory book.

3. An upcoming book by Egbert Rijke.

Additional References

1. Expository articles:

   1. Intuitionistic Type Theory in the Stanford Encyclopedia of Philosophy by Peter Dybjer and Erik Palmgren.

   2. An introduction to Univalent Foundations for Mathematicians, by D. Grayson. Also at arXiv.org.

   3. Homotopy Type Theory and Voevodsky’s Univalent Foundations by Á. Pelayo and M. Warren. Also at arXiv.org. With an ancillary file, tutorial.v, containing the related code (in Coq).

   4. Martin-Löf Complexes by S. Awodey, P. Hofstra, and M. Warren. Also at arXiv.org

2. Courses and Lectures

   1. 15-819 Homotopy Type Theory by Robert Harper
   2. Introduction to Homotopy Type Theory and Univalent Foundations (HoTT/UF) with Agda by Martín Hötzel Escardó.

3. Theses

   1. Egbert Rijke’s Master Thesis
   2. Kuen-Bang Hou (Favonia)’s PhD Thesis.
   3. Guillaume Brunerie’s PhD Thesis.
   4. Evan Cavallo’s Masters Thesis.
   5. Max Blans’ Bachelor Thesis

Agda References

Many of the following references have pointers to installation instructions. See however, install.html for a step-by-step guide.

Documentation

1. Agda wiki
2. The Agda documentation. You may want to start here.
3. Agda further references.

Courses using Agda

1. Programming Language Foundations in Agda by Philip Wadler.
2. CS410-17 (Video lectures) (alternatively here, with Agda exercises and solutions), by Conor McBride.