Homotopy Type Theory and Univalent Foundations meetings
- Thu 18 Dec: Guillaume Brunerie (Univ Nice) - Higher inductive types and synthetic homotopy theory (room: EL42, 10h-11h)
- 5 Dec: Andrea Vezzosi
- 28 Nov: Andrea Vezzosi - Step indexing and the topos of trees. Birkedal Mogelberg Shulman
- Nov 21: Simon Huber - Fundamental group of the circle Licata, Shulman, cub
- Nov 5 : Bassel Mannaa (continued)
- Oct 31: Bassel Mannaa - Categories. Ch 9 / Ahrends, Kapulkin, Shulman
- Oct 24: Bas Spitters - hSets (continued)
- Oct 14, 2014: Bas Spitters - hSets. Sec 10.1 of the book/Rijke Spitters
- Dec 2, 2013: Bassel Mannaa - Sheaf Semantics (continued)
- Nov 13, 2013: Bassel Mannaa - Sheaf Semantics (continued)
- Nov 7, 2013: Bassel Mannaa - Sheaf Semantics
- Mar 13, 2013: Simon Huber - Pre-sheaf models of Type Theory (continued).
- Mar 11, 2013: Simon Huber - Pre-sheaf models of Type Theory.
- Feb 19, 2013: Anders Mörtberg and Cyril Cohen - The univalence axiom and some of its consequences.
- Nov 14, 2012: Peter Dybjer - Models of Type Theory: Categories with families and categories with attributes.
- Nov 13, 2012: Peter Dybjer - Models of Type Theory (continued).
- Nov 9, 2012:
- Cyril Cohen - Informal correspondence between Type Theory and Homotopy Theory (continued).
- Peter Dybjer - Models of Type Theory.
- Nov 6, 2012: Cyril Cohen - Informal correspondence between Type Theory and Homotopy Theory.
- Oct 23, 2012: Planning meeting. Discussed possible topics (see below).
- Guilhem: Inductive types in HoTT
- Jean-Philippe: Isomorphisms and equality + String diagrams (ProgLog talk ?)
- Anders: Formalizing mathematics with univalence
Material and links:
- HoTT blog
- Homotopy type theory and Voevodsky's univalent foundations
- Mike Shulmans HoTT minicourse
- Mike Shulmans HoTT seminar series
- HoTT book