Homotopy type theory

On homotopy type theory (HoTT) and the program of univalent foundations.

Community activity:

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
    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)