Finn Lawler regular fibration (Rev #7)

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 that preserve cartesian arrows, satisfying Frobenius reciprocity and the Beck--Chevalley condition for product-absolute 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 functors $f^*$ .

Our regular fibrations are those of Pavlovic. A similar definition is given by Jacobs, whose only essential difference is that the fibres of a regular fibration are required to be preorders (or equivalently partial orders). Hence such ordered regular 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 subobject fibration $Sub(C) \to C$ (that sends $S \hookrightarrow X$ to $X$ ) is regular.

Proof

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

If $C$ is a regular category, then 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) = Sub(C)_A$ is the identity $1_A$ on $A$ , and binary products in the fibres $Sub(A)$ are given by pullback. The products are preserved by reindexing functors $f^*$ because (the $f^*$ are right adjoints but also because) $f^*(S \wedge S')$ and $f^*S \wedge f^*S'$ have the same universal property. The projection $Sub(C) \to C$ clearly preserves these products. The Beck–Chevalley condition follows from pullback-stability of images in $C$ .

Conversely, suppose $Sub(C) \to C$ is a regular fibration. We need to show that $C$ has equalizers (to get finite limits) and pullback-stable images. But the equalizer of $f, g \colon A \rightrightarrows B$ is $(f,g)^*\Delta$ . For images, let $im f = \exists_f 1$ as in Elephant lemma 1.3.1. Pullback-stability follows from the Beck–Chevalley condition, which holds for all pullback squares in $C$ by Seely, Theorem sec. 8.