BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Algebraic type theory - Steve Awodey\, Carnegie Mellon University
DTSTART:20220830T130000Z
DTEND:20220830T140000Z
UID:TALK177902@talks.cam.ac.uk
CONTACT:Jamie Vicary
DESCRIPTION:A type theoretic universe \nE —> U \nbears an algebraic stru
 cture resulting from the type-forming operations of unit type\, identity t
 ype\, dependent sum\, and dependent product\, \nwhich may be generalized t
 o form the concept of a "Martin-Löf algebra".  A free ML-algebra is then 
 a model of type theory with special properties.  The general theory of suc
 h ML-algebras can be seen as a proof-relevant version of the theory of Zer
 melo-Fraenkel algebras from the algebraic set theory of Joyal & Moerdijk. 
 \n(This is work in progress.)
LOCATION:FW26
END:VEVENT
END:VCALENDAR