Finn Lawler regular fibration (Rev #4, changes)

Showing changes from revision #3 to #4: Added | ~~Removed~~ | ~~Chan~~ged

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, satisfyingFrobenius 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$ .

…