# Contents * contents {:toc} ## Definition A **pre-regular fibration** is a [[nlab:bifibration]] $p \colon E \to B$, where $E$ and $B$ have finite products that are preserved by $p$ and that preserve cartesian arrows, satisfying [[nlab:Frobenius reciprocity]] and the [[nlab: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. ... ## 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 +-- {: .num_prop } ###### Proposition A category $C$ is [[nlab:regular category|regular]] if and only if the subobject fibration $Sub(C) \to C$ (that sends $S \hookrightarrow X$ to $X$) is regular. =-- +-- {: .proof } ###### Proof For our purposes, a regular category is one that has [[nlab:finite limits]] and [[nlab:pullback]]-stable [[nlab:image|images]]. If $C$ is a regular category, then the adjunctions $\exists_f \dashv f^*$ come from pullbacks and images in $C$ ([Elephant](References#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](References#elephant) lemma 1.3.1. Pullback-stability follows from the Beck--Chevalley condition, which holds for all pullback squares in $C$ by [Seely](References#seely83hyper), Theorem sec. 8. =-- [[!redirects regular fibrations]]