Homotopy Type Theory 2015: Presentation topics
Possible topics for presentations
- The general theory of categorical models of type theory: papers by Hofmann and Pitts
- Identity types and weak factorisation systems: Gambino and Garner , Awodey and Warren
- Path object categories, see Van den Berg and Garner and Docherty
- Quillen model categories: various sources, see here
- Groupoid model: Hofmann and Streicher, The groupoid interpretation of type theory. Available here
- The univalent model in simplicial sets, see here
- Model in cubical sets: see Thierry Coquand's homepage, for example, here
- Basics, in particular basic properties of the identity type: Chapters 1 and 2 of the HoTT book
- Types as omega-groupoids: Van den Berg and Garner and Lumsdaine
- Logic and sets in homotopy type theory: Chapter 3 of the HoTT book
- The univalence axiom and function extensionality: Chapter 4 of the HoTT book
- Synthetic homotopy theory: Chapter 8 of the HoTT book
- Category theory in homotopy type theory: Chapter 9 of the HoTT book
Recommended texts on type theory
- Per Martin-Löf. Intuitionistic type theory. Bibliopolis, 1984. Available here.
- Bengt Nordström, Kent Petersson and Jan M. Smith.Programming in Martin-Löf's Type Theory. Oxford University Press, 1990. Available here.
To main page.