Finn Lawler regular fibration (Rev #4)

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$ and by reindexing, 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

For our purposes, a regular category is one that has finite limits? and pullback?-stable images?.

The ‘only if’ part of the proposition is straightforward: the adjunctions $\exists_f \dashv f^*$ come from pullbacks and images in $C$ (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$ .

…