Arithmetic universes and classifying toposes

TL;DR

This paper develops a 2-categorical framework for reasoning about arithmetic universes and classifying toposes, establishing base-independent results and fibrational structures that connect models, toposes, and geometric theories.

Contribution

It introduces a fibrational approach to classifying toposes within the 2-category of contexts for arithmetic universes, generalizing Grothendieck topos results.

Findings

Constructs base-independent topos results with natural numbers objects.

Describes strict actions of categories of models on contexts via Gray tensor product.

Develops a fibrational perspective on classifying toposes as representing objects.

Abstract

Reasoning in the 2-category Con of contexts, certain sketches for arithmetic universes (i.e. list arithmetic pretoposes; AUs), is shown to give rise to base-independent results of Grothendieck toposes, provided the base elementary topos has a natural numbers object. Categories of strict models of contexts $T$ in AUs are acted on strictly on the left by non-strict AU-functors and strictly on the right by context maps, and the actions combine in a strict action of a Gray tensor product. Any context extension $T_0 \subset T_1$ gives rise to a bundle. For each point of $T_0$ - a model $M$ of $T_0$ in an elementary topos $S$ with nno - its fibre is a generalized space, the classifying topos $S[T_1/M]$ for the geometric theory $T_1/M$ of $T_1$-models restricting to $M$. This construction is "geometric" in the sense that for any geometric morphism $f: S' \to S$, the classifier $S'[T_1/f^\ast M]$ is got by pseudopullback of $S[T_1/M]$ along $f$. This is treated in a fibrational way by considering a 2-category GTop of Grothendieck toposes (bounded geometric morphisms) fibred (as bicategory) over a 2-category of elementary toposes with nno, geometric morphisms, and natural isomorphisms. The notion of classifying topos as representing object for a split fibration is then fibred over variable base using fibrations "locally representable" over a second fibration.