Fibrations of AU-contexts beget fibrations of toposes

Sina Hazratpour, Steven Vickers

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 a…