BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Quillen model structures from models of HoTT - Steve Awodey (Depar
 tments of Philosophy and Mathematics\, Carnegie Mellon University)
DTSTART:20201020T131500Z
DTEND:20201020T141500Z
UID:TALK153085@talks.cam.ac.uk
CONTACT:José Siqueira
DESCRIPTION:A Quillen model category satisfying certain additional conditi
 ons can be shown to interpret homotopy type theory\, as does for instance 
 Voevodsky’s model in simplicial sets.\nBut the converse is also true: gi
 ven a certain kind of abstract model of HoTT (as in the work of Orton & Pi
 tts)\, one can endow the underlying category with a Quillen model structur
 e\, as was first shown by Sattler.  A crucial role is played by the princi
 ple of univalence\, which implies that the universe of fibrant objects is 
 itself fibrant\, by an argument due to Coquand.
LOCATION:Zoom (Meeting ID 916 7928 3736\, passcode 844306)
END:VEVENT
END:VCALENDAR