Peter LeFanu Lumsdaine: Equivalences of (models of) type theories
Tid: On 2015-10-07 kl 10.00 - 11.45
Plats: Room 16, building 5, Kräftriket, Department of mathematics, Stockholm University
Medverkande: Peter LeFanu Lumsdaine
Abstract: (joint work with Chris Kapulkin)
I will present a new model of type theory in “span-equivalences” over a given model, based on the model in spans or basic pairs (as given by Simone Tonelli and by Mike Shulman).
This “span-equivalences” model provides a useful technical tool for reasoning about equivalence between models of type theories. I will describe (at least) two applications: firstly, that once the interpretation of contexts, types, and terms has been fixed, the interpretation of the rest of type theory is determined up to equivalence; and secondly, a presentation of the “homotopy theory of models of type theory”.
This is work in progress, and suggestions of further applications are very welcome!