Models of DTT Group Summer 2025

Topics and References

• May 8, 15, 22: Rules of type theory (Ben)
  • (READ THIS ONE) Egbert Rijke, “Introduction to homotopy theory”: Chapters I.1–6; II.11, 13, 17, 20
  • June 6, 2022 draft of Egbert’s book: More stuff, less polish
  • The HoTT Book: Appendix A.2 (or A.1)
  • Martin-Löf, “Intuitionistic type theory”: “Bibliopolis Book”
  • Hofmann, “Syntax and semantics of dependent types”: Syntactic category (“term model”)
• May 29: Categories with families and the groupoid model (Zack)
  • Hofmann, “Syntax and semantics of dependent types”: Categories with families in detail
  • Hofmann-Streicher, “The groupoid interpretation of type theory”
  • Dybjer, “Internal type theory”: Optional, original source of categories with families
• Gambino-Garner and Awodey-Warren (Adrian)
  • Gambino-Garner, “The identity type weak factorization system”
  • Awodey-Warren, “Homotopy theoretic models of identity types”
• The simplicial model (Benni)
  • Kapulkin-Lumsdaine, “The simplicial model of univalent foundations”
• Lumsdaine-Warren (Max)
  • Lumsdaine-Warren, “The local universes model”
• Type-theoretic fibration categories (Benni)
  • Joyal, “Notes on clans and tribes”
  • Shulman, “Univalence for inverse diagrams and homotopy canonicity”: Definition of type-theoretic fibration categories
• Natural models (Ben)
  • Awodey, “Natural models of homotopy type theory”