What I Wish I Knew When Learning HoTT

Auke Booij

This document intends to refer to concepts one may not be aware of on a first reading of the HoTT book, and intends to give a crude, possibly unhelpful intuition for them.

Thanks for additional input from Sina Hazratapour, Manfred Kerber, Ulrik Buchholtz and Andrej Bauer.

Changelog

0.1

first release (?)

Biblography

[AW09]Steve Awodey and Michael A. Warren. Homotopy theoretic models of identity types. Mathematical Proceedings of the Cambridge Philosophical Society, 146(1):45–55, 2009. arXiv:0709.0248, doi:10.1017/S0305004108001783.
[Bau16]Andrej Bauer. Five stages of accepting constructive mathematics. Bulletin of the American Mathematical Society, 2016. doi:10.1090/bull/1556.
[BGL+17]Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, and Bas Spitters. The HoTT library: a formalization of homotopy type theory in Coq. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, 164–172. New York, NY, USA, 2017. ACM. arXiv:1610.04591, doi:10.1145/3018610.3018615.
[Bis70]Errett Bishop. Mathematics as a numerical language. In A. Kino, J. Myhill, and R.E. Vesley, editors, Intuitionism and Proof Theory: Proceedings of the Summer Conference at Buffalo N.Y. 1968, volume 60 of Studies in Logic and the Foundations of Mathematics, pages 53–71. Elsevier, 1970. doi:10.1016/S0049-237X(08)70740-7.
[CCHMortberg17]Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical type theory: a constructive interpretation of the univalence axiom. Linked via the cubicaltt github repository, 2017. URL: http://www.cse.chalmers.se/~coquand/cubicaltt.pdf, arXiv:1611.02108.
[Hof97]Martin Hofmann. Syntax and semantics of dependent types. In Semantics and Logics of Computation, 79–130. Cambridge University Press, 1997.
[Kra13]Nicolai Kraus. The truncation map |_| : ℕ -> ‖ℕ‖ is nearly invertible. Homotopy Type Theory blog, October 2013. URL: https://homotopytypetheory.org/2013/10/28/the-truncation-map-_-\%e2\%84\%95-\%e2\%80\%96\%e2\%84\%95\%e2\%80\%96-is-nearly-invertible/.
[NFS12]Fredrik Nordvall Forsberg and Anton Setzer. A finite axiomatisation of inductive-inductive definitions. In Ulrich Berger, Diener Hannes, Peter Schuster, and Monika Seisenberger, editors, Logic, Construction, Computation, volume 3 of Ontos mathematical logic, pages 259–287. Ontos Verlag, 2012.
[HotzelEscardo18]Martín Hötzel Escardó. A self-contained, brief and complete formulation of Voevodsky’s Univalence Axiom. ArXiv e-prints, March 2018. arXiv:1803.02294.
[LeFanuLumsdaineShulman17]Peter LeFanu Lumsdaine and Michael Shulman. Semantics of higher inductive types. ArXiv e-prints, May 2017. arXiv:1705.07088.
[RiehlShulman17]Emily Riehl and Michael Shulman. A type theory for synthetic ∞-categories. ArXiv e-prints, May 2017. arXiv:1705.07442.
[Shulman15]Michael Shulman. Brouwer’s fixed-point theorem in real-cohesive homotopy type theory. ArXiv e-prints, September 2015. arXiv:1509.07584.