Abstract: Categorifying the comprehension scheme of ZF naturally leads to the notion of the subobjectclassifier, namely the “true” morphism from the terminal object to the object of truth values of the category is the the universal subobject and any subobject is obtained as a pullback of the universal subobject. It also yields the epi-mono factorization system in the category. Going one level higher, it was first realized by Street and Walters () that category of pointed sets discretely opfibred over the category of sets plays the same role as the subobject classifier. This was internalized in suitably structured 2-categories. Similarly the comprehension construction yields that discrete opfibrations and initial functors form a factorization system. There is a dual comprehensive factorization system, namely that of discrete fibrations and finalfunctors. Going yet another dimension higher, we introduce the notion of comprehension construction for bicategories() (that is internal to the tricategory Hom of bicategories, pseudo functors,pseudo natural transformations, and modifications). This will rely on earlier work on fibrationsof bicategories (, , ).
For us, the main example is the bicategory of generalized spaces(that is Grothendieck toposesdefined over a varying elementary base) fibred over the bicategory of elementary toposes and geometric morphisms. We use the structure of comprehension to prove results about fibrations and opfibrations of toposes from fibrational extension of generalized geometric theories (). As we shall see the notions of (op)fibration of toposes have close connections to topological properties. For instance, every local homeomorphism is an opfibration while every fibrewiseS tone space is a fibration.
To study fibrations of toposes, Johnstone defined fibrations internal to 2-categories (). If toposes are taken to be bounded over some fixed baseS, the analysis of fibrations and opfibrationsin the 2-category BTop/S of bounded toposes over a base S is much easier than the general casewhere there is no canonical choice of base topos and one has to work in the 2-categoryBTop.Indeed, Johnstone proved several important (op)fibrational results inBTop.I will introduce the 2-categoryConof Arithmetic Universe (AU) contexts developed by Vickers(, ). It provides a language to reason about geometric construction within the predicativefragment of internal language of toposes, that is within the language of Arithmetic Universes.Borrowing from work of Street (), we introduce a syntactic notion of (op)fibration in Con which is based on Chevalley’s internal characterization of fibrations obtained as a theorem inthere. Note that Johnstone’s definition of internal (op)fibrations is more general than Chevalley’sdefinition: neither strictness of 2-categories nor the existence of the structure of strict pullbacksand comma objects are assumed.
I shall explain our result that gives a recipe for obtaining (op)fibrations of toposes from thefinitary syntactic (op)fibrations of contexts (). The scafolding of the proof of this result isbased on a certain comprehension bicategory involving fibred bicategory of generalized spacesover elementary toposes.As an applications of this result, I will discuss the construction of the colimits of Grothendiecktopos from generalized point-freebag contexts. Hopefully, this sheds some light on the relation-ship between AUs and traditional Grothendieck topos theory.
- Ross Street and Robert Walters, “The comprehensive factorization of a functor”,Bulletin of theAmerican Mathematical Society, vol.791973, 936–941.
- Ross Street, “Fibrations and Yoneda’s lemma in a 2-category”,Lecture Notes in Math., Springer, Berlin,vol.420, 1974, pp. 104-133.
- Peter Johnstone. “Fibrations and partial products in a 2-category”,Applied Categorical Structures,vol.1, 1993, pp. 141–179.
- Claudio Hermida. “Some properties of Fib as a fibred 2-category”,Journal of Pure and Applied Algebra,vol.134, 1999, pp. 83-109
- Igor Bakovic. “Some properties of Fib as a fibred 2-category”,93rd Peripatetic Seminar on Sheaves andLogic, University of Cambridge, 2012
- Mitchell Buckley. “Fibred 2-categories and bicategories”,Journal of Pure and Applied Algebra218, 2014,pp. 1034–1074.
- Steven Vickers. “Sketches for arithmetic universes”, 2016,Journal of Logic and Analysis Accepted for publication June 2018.URL: https://arxiv.org/abs/1608.01559
- Steven Vickers. “Arithmetic universes and classifying toposes”,Cahiers de Topologie et Géométrie Différentielle Catégoriques58(4):213–248, 2017.https://arxiv.org/abs/1701.04611
- Sina Hazratpour and Steven Vickers. “Fibrations of AU-contexts beget fibrations of toposes”Sub-mitted to Theory and Application of Categories (TAC) 2020.URL: https://arxiv.org/abs/1808.08291
- Sina Hazratpour. “A logical study of some 2-categorical aspects of toposes”,PhD thesis, University ofBirmingham, 2020