Proof

For our purposes, a regular category is one that has finite limits and pullback-stable images.

If $C$ is a regular category, then the adjunctions $\exists_f \dashv f^*$ come from pullbacks and images in $C$ (Elephant lemma 1.3.1) as does the Frobenius property (${}$op. cit. lemma 1.3.3). The terminal object of $\mathrm{Sub}(A)=\mathrm{<span><del\; class="diffmod">\; Mon</del><ins\; class="diffmod">\; Sub</ins></span>}(C{)}_A$ Sub(A) = Mon(C)_A Sub(C)_A is the identity $1_A$ on $A$, and binary products in the fibres $Sub(A)$ are given by pullback. The products are preserved by reindexing functors $f^*$ because (the $f^*$ are right adjoints but also because) a cone over the diagram for$f^*(S \wedge S')$ can and be rearranged into a cone over that for$f^*S \wedge f^*S'$ , giving have the two the same universal property. The projection$\mathrm{<span><del\; class="diffmod">\; cod</del><ins\; class="diffmod">\; Sub</ins></span>}(C)\to C$ cod Sub(C) \to C clearly preserves these products. The Beck–Chevalley condition follows from pullback-stability of images in $C$.

Conversely, suppose $\mathrm{<span><del\; class="diffmod">\; Mon</del><ins\; class="diffmod">\; Sub</ins></span>}(C)\to C$ Mon(C) Sub(C) \to C is a regular fibration. We need to show that $C$ has equalizers (to get finite limits) and pullback-stable images. But the equalizer of $f, g \colon A \rightrightarrows B$ is $(f,g)^*\Delta$. For images, let $im f = \exists_f 1$ as in Elephant lemma 1.3.1. Pullback-stability follows from the Beck–Chevalley condition. condition, which holds for all pullback squares in$C$ by Seely, Theorem sec. 8.