You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Tim Hosgood (Jun 02 2021 at 23:49):This Thursday (the 3rd of June) at 17:00 UTC!
Model Structures from Models of HoTT (Steve Awodey)
Homotopical models of Martin-Löf type theory often make use of the notion of a Quillen model category, even if only implicitly. From the interpretation of identities between terms as paths in an abstract space, to the univalence principle identifying identities of types with homotopy equivalences of spaces, the standard tools of abstract homotopy theory provide the means to make rigorous the basic intuition behind the homotopical interpretation of the formal logical system.
So good is this kind of model that it turns out to be possible to invert the process, in a certain sense; given a categorical model of HoTT of an appropriate kind, one can construct from it a full Quillen model structure on the underlying category. This can be seen as a further strengthening of the idea of HoTT as the internal language of an -topos.
YouTube: https://www.youtube.com/watch?v=c0Fwhum4X08
Zoom: https://topos-institute.zoom.us/j/5344862882?pwd=Znh3UlUrek41T3RLQXJVRVNkM3Ewdz09