Till innehåll på sidan

Peter LeFanu Lumsdaine: Inverse diagram models of type theory

Tid: On 2017-11-01 kl 10.00 - 11.45

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

Medverkande: Peter LeFanu Lumsdaine (SU)

Exportera till kalender

Abstract:
*Homotopical inverse diagrams* provide a large class of models of type theory, including:

- spans / relations / basic pairs (cf. Tonnelli/Martin-Löf);
- span-equivalences (cf. PLL seminars from October 2015);
- infinite contexts / spreads (cf. Martin-Löf)
- semi-simplicial types (externally indexed).

Concretely, given any CwA (category with attributes) C and any inverse category I, there is a new CwA C^I, whose contexts consist of C-valued diagrams on I, and whose types are “Reedy types”, i.e. families of types from C in suitable contexts, together constituting a new diagram over I. Compared to general presheaf models, the index category is less general (since it must be an inverse category), but the range CwA is more general: the diagrams can be valued in any other model of type theory, not only in sets or similar categories.
If C carries at least identity types, and I is equipped with a class of “weak equivalences”, then C^I restricts to a submodel C^I_h of “homotopical inverse diagrams”, which again inherits much logical structure from C (though under slightly stronger assumptions than for C^I).
These models have both logical and homotopy-theoretic applications; I will discuss these briefly for motivation, but will mostly focus on the construction of the model itself, and on some open directions for possible generalisation.
(joint work with Chris Kapulkin)
 

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)

- Mike Shulman, Univalence for inverse diagrams and homotopy canonicity, arxiv.org/abs/1203.3253  — a closely analogous construction, for type-theoretic fibration categories instead of CwA’s