Finn Lawler regular fibration (Rev #5, changes)

Showing changes from revision #4 to #5: 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 that are preserved by $p$ and by that ~~reindexing,~~ preserve cartesian arrows, satisfyingFrobenius reciprocity and the Beck--Chevalley condition for pullback squares in $B$ .

The preservation conditions on products are equivalent to requiring that each fibre $E_A$ have finite products and that these be preserved by all reindexing funtors $f^*$ .

Our regular fibrations are those of Pavlovic. A very similar definition is given by Jacobs, whose only essential difference is that the fibres of a regular fibration are required to be preorders. (Hence such fibrations model regular logic where all proofs of the same sequent are considered equal.)

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?~~finite limits and ~~pullback?~~pullback-stable ~~images?~~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 $Sub (A) = Mon (C))_{A}$ ~~Mon(C)~~ Sub(A) = Mon(C)_A is the identity $1_{⊤ A}$ ~~1_\top~~ 1_A on ~~the~~ ~~terminal~~ ~~object~~ of $C A$ C A , and binary products ~~are~~ ~~given~~ by ~~pullbacks~~ in the fibres $C Sub (A)$ C Sub(A) are given by pullback. The products are preserved by reindexing functors $f^*$ because (the $f^*$ are right adjoints but also because) a cone over the diagram for $f^*(S \wedge S')$ can be rearranged into a cone over that for $f^*S \wedge f^*S'$ , giving the two the same universal property. The projection $cod$ clearly preserves these products. The Beck–Chevalley condition follows from pullback-stability of images in $C$ .

…