Recent Changes - Search:
ProgLog /

HoTT

Homotopy Type Theory and Univalent Foundations meetings

Upcoming meetings:

  • Thu 18 Dec: Guillaume Brunerie (Univ Nice) - Higher inductive types and synthetic homotopy theory (room: EL42, 10h-11h)

Past meetings:

  • 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).

Possible topics:

  • Guilhem: Inductive types in HoTT
  • Jean-Philippe: Isomorphisms and equality + String diagrams (ProgLog talk ?)
  • Anders: Formalizing mathematics with univalence

Material and links:

The mailing list associated to these meetings is htt101@lists.chalmers.se (subscribe)