BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Category Theory Seminar
SUMMARY:Large categories and quantifiers in topos theory -
  Michael Shulman (University of San Diego)
DTSTART;TZID=Europe/London:20210126T161500
DTEND;TZID=Europe/London:20210126T171500
UID:TALK156685AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/156685
DESCRIPTION:The internal logic of an elementary topos E makes 
 it easy to "do mathematics" relative to E\, with a
 n automatic way to interpret types as objects of E
 .  But it is unable to deal with large objects suc
 h as proper classes\, indexed categories\, or form
 ulas with unbounded quantifiers.  We can solve thi
 s problem by embedding E in its category of stacks
  of groupoids\, whose internal logic is Martin-Lof
  dependent\ntype theory with "1-truncated homotopy
 ".  This allows us to\nautomatically translate sta
 ndard theorems of category theory into the analogo
 us facts about indexed categories\, and to formula
 te topos-theoretic analogues of unbounded axiom sc
 hemas such as separation and replacement.\n\nZoom 
 link: \n https://maths-cam-ac-uk.zoom.us/j/9437534
 6045?pwd=QlI3WFB2WFRhV1RzZzdyOHFVZk95dz09\n\nMeeti
 ng ID 943 7534 6045\, passcode 252455
LOCATION:Zoom (Meeting ID 943 7534 6045\, passcode 252455)
CONTACT:José Siqueira
END:VEVENT
END:VCALENDAR
