Homotopy type theory

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
  1. 2014: Subsystems and regular quotients of C-systems (arxiv)
  2. 2014: C-system of a module over a monad on sets (arxiv)
  3. 2014: A C-system defined by a universe category (arxiv)
  4. 2015: Products of families of types in the C-systems defined by a universe category (arxiv). Evolved into three TAC papers:
     • 2016: Products of families of types and \((\Pi,\lambda)\)-structures on C-systems (arxiv, pdf)
     • 2017: C-systems defined by universe categories: presheaves (arxiv, pdf)
     • 2017: The \((\Pi,\lambda)\)-structures on the C-systems defined by universe categories (arxiv, pdf)
  5. 2015: Martin-Lof identity types in the C-systems defined by a universe category (arxiv)
  6. 2015: Lawvere theories and C-systems (arxiv)
  7. 2016: Lawvere theories and Jf-relative monads (arxiv)
  8. 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)