Fibrations of AU-contexts beget fibrations of toposes

TL;DR

This paper explores how fibrations in the context of arithmetic universes induce fibrations in topos theory, providing criteria and reformulations relevant to categorical logic and topos theory.

Contribution

It establishes a connection between fibrations of AU-contexts and fibrations of toposes, offering a new reformulation of Johnstone's criterion.

Findings

Fibrations of AU-contexts induce fibrations of toposes.

Provides a reformulation of Johnstone's criterion.

Establishes conditions under which extension maps satisfy Chevalley criteria.

Abstract

Suppose an extension map $U\colon \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\colon\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.