Showing changes from revision #8 to #9: Added | Removed | Changed

Contents

Definition

A pre-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 of types C, D and E in $B$. A regular fibration is a pre-regular fibration that also satisfies the Beck–Chevalley condition for type-B squares.

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^*$.

The type-A Beck–Chevalley condition

Here and in my thesis I originally required regular fibrations to satisfy the type-A BC condition, but I now believe that it holds automatically as long as E does.

By Shulman’s construction, a pre-regular fibration $E$ over $B$ gives rise to a cartesian equipment $B \to Matr(E)$, and hence a cartesian bicategory $Matr(E)$. Type-E squares in the bicategory are exact because they satisfy the BC condition in the fibration. $Matr(E)$ then becomes compact closed bicategory, which is to say that there is an equivalence $hom(A \times B, C) \simeq hom(A, C \times B)$ given by composing with $A \times d_\bullet e^\bullet$ (left to right) and with $C \times d^\bullet e_\bullet$ (right to left), where $d$ is the diagonal at $B$ and $e$ the map from $B$ to the terminal object. We will write this as $R^\wedge \colon A \to C \times B$ for $R \colon A \times B \to C$ and $S^\vee \colon A \times B \to C$ for $S \colon A \to C \times B$. Similarly there is an equivalence $hom(A \times B, C) \simeq hom(B, A \times C)$, which we will write as ${}^\wedge T$ and ${}^\vee U$. If $R \colon A \to B$ then $R^\circ = {}^\vee (R^\wedge) \cong {}^\wedge (R^\vee)$. The type-E BC condition implies that $f_\bullet \dashv f_\bullet^\circ$, and therefore $f_\bullet^\circ \cong f^\bullet$, and also that $d_\bullet^\vee \cong d^\bullet$ and $(d^\bullet)^\wedge \cong d_\bullet$.

The claim now is that modulo these isomorphisms, the morphisms required to be invertible by exactness of or BC for type-A squares are equal to $\beta_1 = (d_\bullet f_\bullet \cong (f \times f)_\bullet d_\bullet)^\vee$ and $\beta_2 = {}^\wedge \beta_1$. Being the images under equivalences of invertible morphisms, then, they must themselves be invertible.

… The following pictures show the essential parts of the proof using string diagrams, which can be read top-to-bottom as morphisms in a cartesian bicategory or bottom-to-top as objects in a monoidal bifibration as inthis paper.

Logic

A regular fibration posesses exactly the structure needed to interpret regular logic, i.e. the ${\exists}{\wedge}{\top}$-fragment of first-order logic.

…

Characterization