Finn Lawler regular fibration (Rev #3)

Definition
Logic
Characterization

Definition

A regular fibration is a bifibration $p \colon E \to B$ , where $E$ and $B$ have finite products preserved by $p$ , satisfying Frobenius reciprocity and the Beck--Chevalley condition for pullback squares in $B$ .

Logic

A regular fibration posesses exactly the structure needed to interpret regular logic?.

…

Characterization

Proposition

A category $C$ is 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

…