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, June 5, 12, 26: Categories with families/attributes (Zack)
  • (READ THIS ONE) Hofmann, “Syntax and semantics of dependent types”: Categories with families in detail
  • Dybjer, “Internal type theory”: Optional, original source of categories with families
• July 3: The groupoid model (Adrian)
  • Hofmann-Streicher, “The groupoid interpretation of type theory”

Future Topics

• Gambino-Garner, “The identity type weak factorization system”
• Awodey-Warren, “Homotopy theoretic models of identity types”
• Kapulkin-Lumsdaine, “The simplicial model of univalent foundations”
• Lumsdaine-Warren, “The local universes model”
• Joyal, “Notes on clans and tribes”
• Shulman, “Univalence for inverse diagrams and homotopy canonicity”
• Awodey, “Natural models of homotopy type theory”