Till innehåll på sidan

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

Exportera till kalender

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!