University of Cambridge > Talks.cam > Category Theory Seminar > Large categories and quantifiers in topos theory

Large categories and quantifiers in topos theory

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact José Siqueira.

The internal logic of an elementary topos E makes it easy to “do mathematics” relative to E, with an automatic way to interpret types as objects of E. But it is unable to deal with large objects such as proper classes, indexed categories, or formulas with unbounded quantifiers. We can solve this problem by embedding E in its category of stacks of groupoids, whose internal logic is Martin-Lof dependent type theory with “1-truncated homotopy”. This allows us to automatically translate standard theorems of category theory into the analogous facts about indexed categories, and to formulate topos-theoretic analogues of unbounded axiom schemas such as separation and replacement.

Zoom link: https://maths-cam-ac-uk.zoom.us/j/94375346045?pwd=QlI3WFB2WFRhV1RzZzdyOHFVZk95dz09

Meeting ID 943 7534 6045 , passcode 252455

This talk is part of the Category Theory Seminar series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2021 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity