# Contents * contents {:toc} ## Definition A **regular fibration** is a [[nlab:bifibration]] $p \colon E \to B$, where $E$ and $B$ have finite products, with those in $E$ preserved by reindexing ($f^*A \times f^*B \cong f^*(A \times B)$), 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 ... =-- [[!redirects regular fibrations]]