# Contents * contents {:toc} ## Definition A **regular fibration** is a [[nlab:bifibration]] $p \colon E \to B$, where $E$ and $B$ have finite products preserved by $p$ and by reindexing, satisfying [[nlab:Frobenius reciprocity]] and the [[nlab:Beck--Chevalley condition]] for pullback squares in $B$. ## 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 [[finite limits]] and [[pullback]]-stable [[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 $Mon(C)$ is the identity $1_\top$ on the terminal object of $C$, and binary products are given by pullbacks in $C$. ... =-- [[!redirects regular fibrations]]