Finn Lawler regular fibration (Rev #2)

Definition
Logic
Characterization

Definition

A regular fibration is a 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 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

…