This page collects resources on the connection between type theory and homotopy theory. If you know of one, please let me know.
- Vladimir Voevodsky’s Univalent Foundations page contains notes and lectures on the homotopy-theoretic foundations of mathematics.
- Vladimir Voevodsky’s github repository with his development of univalent foundations in Coq.
- Andrej Bauer’s github repository of Coq files, including a clone of Vladimir’s files, a tutorial on Coq, and other files.