Finn Lawler regular fibration (Rev #3, changes)

Showing changes from revision #2 to #3: 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,~~ products ~~with~~ preserved ~~those~~ by in $E p$ E p , ~~preserved~~ satisfying 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

…