Fibration of contexts beget fibrations of toposes

Theory and Application of Categories (TAC), 2020

Sina Hazratpour, Steve Vickers. "Fibration of contexts beget fibrations of toposes " Theory and Application of Categories (TAC), 35(16), pages 562–593, 2020, online access


We introduce a notion of (op)fibration in the 2-category Con of contexts. We give a new characterization of weak fibrations internal in 2-categories. Using this characterization, we establish that a context extension $\mathrm{T_1} \to \mathrm{T_0} $ with (op)fibration property and a model $M$ of $\mathrm{T_0}$ in an elementary topos $\mathcal{S}$ with natural number object gives rise to an (op)fibration of elementary toposes with codomain $\mathcal{S}$.


For many special constructions of topological spaces (which for us will be point-free, and generalized in the sense of Grothendieck), a structure preserving morphism between the presenting structures gives a map between the corresponding spaces. Two very simple examples are: a function $f \maps X \to Y$ between sets already is a map between the corresponding discrete spaces; and a homomorphism $f\maps K \to L$ between two distributive lattices gives a map in the opposite direction between their spectra. The covariance or contravariance of this correspondence is a fundamental property of the construction.

In topos theory we can relativize this process: a presenting structure in an elementary topos $\mathcal{E}$ will give rise to a bounded geometric morphism $p\maps \mathcal{F} \to \mathcal{E}$, where $\mathcal{E}$ is the topos of sheaves over $\mathcal{E}$ for the space presented by the structure. Then we commonly find that the covariant or contravariant correspondence mentioned above makes every such $p$ an opfibration or fibration in the 2-category of toposes and geometric morphisms.

If toposes are taken as bounded over some fixed base $\mathcal{S}$, in the 2-category $\mathbf{BTopos}/\mathcal{S}$, then there are often easy proofs got by showing that the generic such p, taken over the classifying topos for the relevant presenting structures, is an (op)fibration. See [SVW13] for some simple examples.

In the 2-category $\mathbf{ETopos}$ of arbitrary elementary toposes with nno, the properties are stronger (because there are more 2-cells) and much harder to prove. In this paper our main result (Theorem 7.2) is to show how to use the arithmetic universe techniques to get simple proofs in the generic style of the sharper, base-independent (op)fibration results in $\mathbf{ETopos}$.

Suppose $U \maps \mathrm{T_1} \to \mathrm{T_0} $ is an extension map in $\mathbf{Con}$, and $M$ is a model of $\mathrm{T_0}$ in $\mathcal{S}$, an elementary topos with nno. Then there is a geometric theory $\mathrm{T_1}/M$, of models of $\mathrm{T_1} $ whose $\mathrm{T_0}$-reduct is $M$, and so we get a classifying topos $p\maps \mathcal{S}[\mathrm{T_1}/M] \to \mathcal{S}$.

We prove that if $U$ is an (op)fibration, then so is $p$ in the sense of [Joh93].

Leave a Comment