Skip to main content

Peter LeFanu Lumsdaine: Inverse diagram models of type theory, II

Time: Wed 2017-11-08 10.00 - 11.45

Location: Room 16, building 5 kräftriket, Department of Mathematics, Stockholm University

Participating: Peter LeFanu Lumsdaine (SU)

Export to calendar

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)

To the calendar