Peter LeFanu Lumsdaine: Inverse diagram models of type theory, II
Tid: On 2017-11-08 kl 10.00 - 11.45
Plats: Room 16, building 5 kräftriket, Department of Mathematics, Stockholm University
Medverkande: Peter LeFanu Lumsdaine (SU)
Abstract:
Last week, I motivated and set up *inverse diagram models* of type theory. This week, I will generalise these to *homotopical* inverse diagram models, providing a much larger class of models, and some fun technical challenges.
References:
- Chris Kapulkin, Peter LeFanu Lumsdaine, The homotopy theory of type theories, arxiv.org/abs/1610.00037 — some examples of the construction (in Section 5), and our major motivating application.
(Section 6)(joint work with Chris Kapulkin)