simplicial type theory reading group

Meeting coordinates: in person at Dal (details TBD), with an online option.

We will study a type theory for synthetic ∞-categories, reviewing basic type theory and ∞-category theory and following it by the more recent paper Directed univalence in simplicial homotopy type theory .

We will alternate speakers for the seminar in the first few weeks, and eventually decide together on how to go over the paper.

• Sept 22: categorical semantics of MLTT. (daniel)
• Sept 29: intro to HoTT, identitity types, path induction. (Deni)notes
• Oct 06: HoTT in Agda workshop. (Jeremiah) worksheet

references:

• The HoTT Book
• Egbert Rijke, Introduction to Homotopy Type Theory..
• Emily Riehl, ∞-Category Theory for Undergraduates. (talk)