BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Large categories and quantifiers in topos theory - Michael Shulman
  (University of San Diego)
DTSTART:20210126T161500Z
DTEND:20210126T171500Z
UID:TALK156688@talks.cam.ac.uk
CONTACT:José Siqueira
DESCRIPTION:The internal logic of an elementary topos E makes it easy to "
 do mathematics" relative to E\, with an automatic way to interpret types a
 s objects of E.  But it is unable to deal with large objects such as prope
 r classes\, indexed categories\, or formulas with unbounded quantifiers.  
 We can solve this problem by embedding E in its category of stacks of grou
 poids\, whose internal logic is Martin-Lof dependent\ntype theory with "1-
 truncated homotopy".  This allows us to\nautomatically translate standard 
 theorems of category theory into the analogous facts about indexed categor
 ies\, and to formulate topos-theoretic analogues of unbounded axiom schema
 s such as separation and replacement.\n\nZoom link: \n https://maths-cam-a
 c-uk.zoom.us/j/94375346045?pwd=QlI3WFB2WFRhV1RzZzdyOHFVZk95dz09\n\nMeeting
  ID 943 7534 6045\, passcode 252455
LOCATION:Zoom (Meeting ID 943 7534 6045\, passcode 252455)
END:VEVENT
END:VCALENDAR