Suppose an extension map U: T_1 -> T_0 in the 2-category Con of contexts for arithmetic universes satisfies a Chevalley criterion for being an (op)fibration in Con. If M is a model of T_0 in an elementary topos S with nno, then the classifier p: S[T_1/M] -> S satisfies the representable definition of being an (op)fibration in the 2-category ETop of elementary toposes (with nno) and geometric morphisms.
Keywords: internal fibration, 2-fibration, context, bicategory, elementary topos, Grothendieck topos, arithmetic universe
2020 MSC: 18D30, 03G30, 18F10, 18C30, 18N10.
Theory and Applications of Categories, Vol. 35, 2020, No. 16, pp 562-593.
Published 2020-04-29.
TAC Home