The inaugural HoTTEST of Spring 2020 will be given by Simon Henry on January 23 at 11:30 Eastern.
Zoom Link: https://zoom.us/j/994874377
I will explain how to any model category, one can associate a first order language which allows to formulate properties of its fibrant objects that are automatically invariant under homotopies and weak equivalences. For example, the special case of the folk model structure on Cat reproduce the well known result that a first order statement about categories not involving equality of objects is invariant under isomorphisms and equivalences of categories. The construction I will present generalizes this to any model category, for example to spaces or quasi-categories.
Though it does not explicitly use it, this is strongly inspired from Makkai's FOLDS and shed a slightly new light on the connection between dependent type theory and homotopy theory.Updated on Jan 21, 2020 01:16 PM PST
Current Colloquia & Seminars