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:

- HoTT blog
- Homotopy type theory and Voevodsky's univalent foundations
- Mike Shulmans HoTT minicourse
- Mike Shulmans HoTT seminar series
- HoTT book

The mailing list associated to these meetings is `htt101@lists.chalmers.se`

(subscribe)