# Homotopy Type Theory Seminar # ## Chapman University, Fall 2024 ## Contact: Jonathan Weinberger, jweinberger@chapman.edu <font color=#f00> **The seminar has concluded for fall 2024.** </font> ~~Mondays, 215--315 (+/- epsilon) Room: KC370 (next to Math lounge)~~ ### Mode of the seminar ### Each meeting, we will discuss a new portion of Emily's lecture notes. Feel free to also consult the other resources mentioned below or search your own. Occasionally, I will recommend other sources like YouTube videos. ### Learning goals ### Most of the topics are concerned with working *within* homotopy type theory, but we also have some later topics on the homotopical-categorical semantics. The overall goals are: * introduce and get familiar with dependent Martin-Löf type theory (MLTT), in particular identity types * learn about weak equivalences between and contractibility of types * introduce Voevodsky's univalence axiom, leading to homotopy type theory (HoTT) as an extension of HoTT * learn about higher inductive types (HITs) using the circle $\mathrm{S}^1$ as an example * define homotopy groups of types and prove $\pi_1\mathrm{S}^1 \simeq \mathbb Z$ * learn about general categorical semantics of MLTT * introduce Voevodsky's simplicial model as the "standard model" of HoTT ### Suggested list of topics ### 1. **Sep 9:** Martin-Löf's Dependent Type Theory ([Rie1] Aug. 30) 2. **Sep 16:** Dependent function types and the natural numbers ([Rie1] Sep. 1) & [Computerphile video with T. Altenkirch (~15 min)](https://www.youtube.com/watch?v=qT8NyyRgLDQ) 3. **Sep 23:** More on dependent function types and the natural numbers ([Rie1] Sep. 1), some inductive and identity types ([Rie1] Sept. 13 & 15) 4. **Sep 30:** More identity types and universes ([Rie1] Sep. 20 & 22) 5. Equivalences, contractibility ([Rie1] Oct. 4, 6 & 11) 6. Truncation levels and function extensionality ([Rie1] Oct 13 & 18) 7. Universal properties and propositional truncation ([Rie1] Oct 20, 25 & 27) 8. The univalence axiom and groups in univalent mathematics ([Rie1] Nov 1 & Nov 8) 9. The circle and its universal cover ([Rie1] Nov 17 & 29) 10. Homotopy groups of types ([Rie1] December 1 & 6) 11. Semantics I: A categorical semantics of dependent type theory ([Rie2] Lecture I) 12. Semantics II: The simplicial model of univalent foundations ([Rie2] Lecture II) ### Optional/additional topics ### *Additional references can be provided for these topics* * Philosophical questions about foundations: set theory v type theory; usability, safety...? Cf. also Liquid Tensor Experiment * H.O.T.T. (higher observational TT) * Structure Identity Principles * Formalization and proof assistants for HoTT * Μοre synthetic homotopy theory * Higher group theory * Cubical type theory * Modalities in HoTT * Simplicial HoTT \& synthetic ∞-categories * ... ### Bibliography ### * [Awo] Steve Awodey (2012). *Type Theory and Homotopy.*, In: Dybjer, P., Lindström, S., Palmgren, E., Sundholm, G. (eds) Epistemology versus Ontology. Logic, Epistemology, and the Unity of Science, vol 27. Springer, Dordrecht. [arXiv:1010.1810](https://arxiv.org/abs/1010.1810) * [Gra] Grayson, Daniel R. (2018). "An introduction to univalent foundations for mathematicians". Bulletin of the American Mathematical Society. 55 (4): 427–450. [arXiv:1711.01477](arXiv:1711.01477). * [Rie1] Emily Riehl (2012). *Course notes on homotopy type theory*, https://github.com/emilyriehl/721/blob/master/721lectures.pdf * [Rie2] Emily Riehl (2024). *On the ∞-topos semantics of homotopy type theory*, Bulletin of the London Mathematical Society, Volume 56, Issue 2, 461-879, [arXiv:2212.06937](https://arxiv.org/abs/2212.06937) * [Rij] Egbert Rijke (2022). *Introduction to homotopy type theory*, book to appear [arXiv:2212.11082](https://arxiv.org/abs/2212.11082) * [Shu] Michael Shulman (2012). *Homotopy type theory: the logic of space*, in *New Spaces in Mathematics: Formal and Conceptual Reflections.* Ed. by Mathieu Anel and Gabriel Catren (2021): 322-404. * [UF] The Univalent Foundations Program (2013). *Homotopy Type Theory: Univalent Foundations of Mathematics*, Institute for Advanced Study, https://homotopytypetheory.org/book