You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Tim Hosgood (May 13 2021 at 16:25):starting in 35 minutes (sorry for the late notification!)
Tim Hosgood (May 13 2021 at 16:26):Abstract:
In this talk we report fundamental results concerning free completions with quotients of specific Lawvere doctrines for building toposes, quasi-toposes and predicative versions of them. Our final goal is to use such completions for modelling foundations of constructive and classical mathematics which are predicative in the sense of Poincaré, Weyl and Feferman, including that in [M09]. We first recall how the tool of completing an elementary existential Lawvere doctrine with exact quotients is the fundamental construction behind the tripos-to-topos construction in [HJP80] beside including as instances both the exact completion of a regular category and that of a weakly lex finite product category, as reported in [MR15]. We then describe recent work with Fabio Pasquali and Pino Rosolini where we show how the elementary quotient completion of an elementary Lawvere doctrine in [MR13] is the fundamental construction behind a tripos-to-quasi-topos construction including toposes as exact completions of a left exact category in [Me03] as instances. We also mention a joint work with Davide Trotta where we extend results in [MPR17] about tripos-to-topos constructions coinciding with exact completions of a left exact category. We end by applying the elementary quotient completion to build examples of predicative toposes including the Effective Predicative Topos in [MM21].
References
[HJP80] J.M. Hyland, P. T. Johnstone and A.M.Pitts. Tripos theory. Math. Proc. Cambridge Philos. Soc. 88, 205-232, 1980
[M09] M.E. Maietti. A minimalist two-level foundation for constructive mathematics. Annals of Pure and Applied Logic, 160(3): 319-354, 2009
[MR13] M.E. Maietti and G. Rosolini. Elementary quotient completion. Theory and Applications of Categories, 27(17): 445–463, 2013
[MR15 ] M.E. Maietti and G. Rosolini. Unifying Exact Completions. Applied Categorical Structures 23(1): 43-52, 2015
[MPR17] M.E. Maietti, F. Pasquali and G. Rosolini. Triposes, exact completions, and Hilbert's ε-operator. Tbilisi Mathematical Journal. 10(3): 141-66, 2017
[Me03] M. Menni. A characterization of the left exact categories whose exact completions are toposes. Journal of Pure and Applied Algebra, 3(177): 287-301, 2003
[MM21] M.E. Maietti, S. Maschio. A predicative variant of Hyland's Effective Topos. To appear in The Journal of Symbolic Logic
Tim Hosgood (May 13 2021 at 16:26):Zoom: https://topos-institute.zoom.us/j/5344862882?pwd=Znh3UlUrek41T3RLQXJVRVNkM3Ewdz09
YouTube: https://www.youtube.com/watch?v=yZvzm_-M0rc