Homotopy type theory
On homotopy type theory (HoTT) and the program of univalent foundations.
Community activity:
- Voevodsky Memorial Conference (2018)
- Videos from IAS, loosely organized
- Andrej Bauer’s course materials on HoTT
- Mike Shulman on what’s so HoTT about formalization
Literature
The HoTT section of the nLab has a large bibliography .
General
- IAS, 2013: Homotopy Type Theory (pdf)
- Shulman, 2017: Homotopy type theory: the logic of space (arxiv, n-Cat Cafe )
- Written “from the perspective of a mathematician wanting to use [type theory] as an internal language for categories”
- Ladyman & Presnell, 2014: A primer on HoTT: Part 1: Formal type theory (pdf)
- Grayson, 2018, in AMS Bulletin: An introduction to univalent foundations for
mathematicians (arxiv, doi, pdf)
- The most readable introduction I know of
Contextual categories
Voevodsky re-axiomatized Cartmell’s contextual categories as C-systems.
- Voevodsky’s incomplete “Notes on Type Systems” (old and new versions)
- Voevodsky’s series of eight papers based on his notes
- 2014: Subsystems and regular quotients of C-systems (arxiv)
- 2014: C-system of a module over a monad on sets (arxiv)
- 2014: A C-system defined by a universe category (arxiv)
- 2015: Products of families of types in the C-systems defined by a universe category (arxiv). Evolved into three TAC papers:
- 2015: Martin-Lof identity types in the C-systems defined by a universe category (arxiv)
- 2015: Lawvere theories and C-systems (arxiv)
- 2016: Lawvere theories and Jf-relative monads (arxiv)
- 2016: C-system of a module over a Jf-relative monad (arxiv)
- Kapulkin & Lumsdaine, 2016: The simplicial model of univalent foundations
(after Voevodsky) (arxiv)
- Mostly expository, explaining the main ideas of V’s work
- Helpful perspective in Sec 1.2: Contextual categories
- Awodey, 2016: Natural models of homotopy type theory (doi, arxiv)
- Ahrens et al, 2021: B-systems and C-systems are equivalent (arxiv)