# 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 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 funtors $f^*$. Our regular fibrations are those of [Pavlovic](References#pavlovic96maps). A very 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. (Hence such 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 projection $cod \colon Mon(C) \to C$ sending $S \hookrightarrow X$ to $X$ is a regular fibration, where $Mon(C)$ is the full subcategory of $C^{\to}$ on the monomorphisms. =-- +-- {: .proof } ###### Proof For our purposes, a regular category is one that has [[nlab:finite limits]] and [[nlab:pullback]]-stable [[nlab:image|images]]. The 'only if' part of the proposition is straightforward: 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) = Mon(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 be rearranged into a cone over that for $f^*S \wedge f^*S'$, giving the two the same universal property. The projection $cod$ clearly preserves these products. The Beck--Chevalley condition follows from pullback-stability of images in $C$. ... =-- [[!redirects regular fibrations]]