Fibrations of AU-contexts beget fibrations of toposes

Abstract

Suppose an extension map $U:{\mathbb{T}}_1\to {\mathbb{T}}_0$ in the 2-category $\mathfrak{Con}$ of contexts for arithmetic universes satisfies a Chevalley criterion for being an (op)fibration in $\mathfrak{Con}$. If $M$ is a model of ${\mathbb{T}}_0$ in an elementary topos $\mathcal{S}$ with nno, then the classifier $p:\mathcal{S}[{\mathbb{T}}_1/M]\to \mathcal{S}$ satisfies Johnstone's criterion for being an (op)fibration in the 2-category $\mathcal{E}\mathfrak{Top}$ of elementary toposes (with nno) and geometric morphisms. Along the way, we provide a convenient reformulation of Johnstone's criterion.

43 pages, about 50 diagrams