# Contents * contents {:toc} ## Definition A **regular fibration** is a [[nlab:bifibration]] $p \colon E \to B$, where $E$ and $B$ have finite products that are preserved by $p$ and that preserve cartesian arrows, satisfying [[nlab:Frobenius reciprocity]] and the [[nlab:Beck--Chevalley condition]] for [[product-absolute pullback]] squares in $B$. The preservation conditions on products are equivalent to requiring that each fibre $E_A$ have finite products and that these be preserved by all reindexing functors $f^*$. Our regular fibrations are those of [Pavlovic](References#pavlovic96maps). A similar definition is given by [Jacobs](References#jacobs99cltt), whose only essential difference is that the fibres of a regular fibration are required to be preorders (or equivalently partial orders). Hence such **ordered regular fibrations** model regular logic where all proofs of the same sequent are considered equal. ## Logic A regular fibration posesses exactly the structure needed to interpret [[regular logic]]. ... ## Characterization +-- {: .num_prop } ###### Proposition A category $C$ is [[nlab:regular category|regular]] if and only if the subobject fibration $Sub(C) \to C$ (that sends $S \hookrightarrow X$ to $X$) is regular. =-- +-- {: .proof } ###### Proof For our purposes, a regular category is one that has [[nlab:finite limits]] and [[nlab:pullback]]-stable [[nlab:image|images]]. If $C$ is a regular category, then the adjunctions $\exists_f \dashv f^*$ come from pullbacks and images in $C$ ([Elephant](References#elephant) lemma 1.3.1) as does the Frobenius property (${}$_op. cit._ lemma 1.3.3). The terminal object of $Sub(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) $f^*(S \wedge S')$ and $f^*S \wedge f^*S'$ have the same universal property. The projection $Sub(C) \to C$ clearly preserves these products. The Beck--Chevalley condition follows from pullback-stability of images in $C$. Conversely, suppose $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](References#elephant) lemma 1.3.1. Pullback-stability follows from the Beck--Chevalley condition, which holds for all pullback squares in $C$ by [Seely](References#seely83hyper), Theorem sec. 8. =-- [[!redirects regular fibrations]]