**Update**: my Ph.D. thesis is now at the [arXiv](http://arxiv.org/abs/1502.08017). Below is the abstract and a brief summary. # Fibrations of predicates and bicategories of relations ## Abstract We reconcile the two different category-theoretic semantics of regular theories in predicate logic. A 2-category of _regular fibrations_ is constructed, as well as a 2-category of _regular proarrow equipments_, and it is shown that the two are equivalent. A regular equipment is a _cartesian equipment_ satisfying certain axioms, and a cartesian equipment is a slight generalization of a cartesian bicategory. This is done by defining a tricategory $Biprof$ whose objects are bicategories and whose morphisms are category-valued profunctors, and then defining an _equipment_ to be a pseudo-monad in this tricategory. The resulting notion of equipment is compared to several existing ones. Most importantly, this involves showing that every pseudo-monad in $Biprof$ has a _Kleisli object_. A strict 2-category of equipments, over locally discrete base bicategories, is identified, and cartesian equipments are defined to be the cartesian objects in this 2-category. Thus cartesian equipments themselves form a 2-category, and this is shown to admit a 2-fully-faithful functor from the 2-category of regular fibrations. The cartesian equipments in the image of this functor are characterized as those satisfying certain axioms, and hence a 2-category of _regular equipments_ is identified that is equivalent to that of regular fibrations. It is then shown that a regular fibration admits _comprehension_ for predicates if and only if its corresponding regular equipment admits _tabulation_ for morphisms, and further that the presence of tabulations for morphisms is equivalent to the existence of _Eilenberg--Moore objects_ for co-monads. We conclude with a brief examination of the two different constructions of the effective topos, via triposes and via assemblies, in the light of the foregoing. ## Outline ### Regular theories and fibrations This is standard stuff, mostly: regular logic is the fragment of first-order logic with only $\exists$, $\wedge$ and $\top$, and a model of it is a [[regular fibration]]. ### The tricategory $Biprof$ We want to define the [[nlab:tricategory]] $BiProf$ of bicategories and profunctors; we need to know what the following things are: 1. [[2-extranatural transformation]] 1. [[2-end]] 1. [[free 2-cocompletion]] and then we define $BiProf$ as [[biprofunctor|here]], and prove that it has Kleisli objects for pseudo-monads. ### The 2-category of equipments We can define an equipment to be a pseudo-monad in $Biprof$, and an equipment functor to be a (representable) monad (op-)morphism. The existence of Kleisli objects in $Biprof$ ensures that these definitions recover those of Wood in [Wood82](References#wood82proarrowsi) and [Wood85](References#wood85proarrowsii). They also have a clear relationship to some of the later ideas in [CKVW](References#ckvw98change). This is fine as far as it goes, but it gives us the wrong kind of 2-cell (what we get is not lax enough). So instead we show that our equipments and their morphisms form an ordinary category that is equivalent to the category underlying [Shulman's](References#shulman08framed) strict 2-category of [[nlab:framed bicategories]] and their morphisms. Then we can say that an equipment 2-cell is a framed transformation between corresponding framed functors. That's a bit of a swindle, but the alternative would be to develop a whole theory of 'doubly-lax' monad morphisms and lax monad 2-cells and so on. It ought to be done, certainly, but not here by us, simply because it would take too long. ### Cartesian equipments and regular fibrations We have a 2-category of equipments now, and it clearly has finite products, so we define a cartesian equipment to be a cartesian object in it. That's a monoid object whose multiplication and unit maps are right adjoint to the diagonal and terminal maps. So we get a 2-category $CartEqt$. When we spell out what it means for an equipment to be cartesian, it becomes obvious that a bicategory $\mathcal{B}$ is a cartesian bicategory if and only if $Map(\mathcal{B}) \to \mathcal{B}$ is a cartesian equipment. As in [Shulman08](References#shulman08framed), from a regular fibration $E$ over some category $B$ we can construct a cartesian equipment $Matr(E)$ (of 'matrices' in $E$): its objects are those of $B$, its vertical/tight maps are the morphisms of $B$ and the category of horizontal maps and (globular) cells from $b$ to $b'$ is $E(b \times b')$. The important point now is that $E \mapsto Matr(E)$ is a fully faithful functor $RegFib \to CartEqt$. If $B \to \mathcal{B}$ is a cartesian equipment, then $Pred(\mathcal{B}) = \mathcal{B}(-_\bullet, \mathbf{1})$ is a bifibration, where $f_\bullet$ is the morphism in $\mathcal{B}$ arising from a morphism $f$ in $B$, and $\mathbf{1}$ is the terminal object of $B$. In fact, it is almost a regular fibration: there are two Beck--Chevalley conditions required, one corresponding exactly to the notion of a separable object in a cartesian bicategory. The other has the Frobenius condition familiar from cartesian bicategories as a special case, but seems to be strictly more general. +-- {: .standout } **Later comment**: I now think that the condition for [[product-absolute pullback|type-A squares]] follows from the condition for diagonal-coassociativity squares (the 'Frobenius law' of Carboni and Walters), in both cartesian bicategories and 'pre-regular' fibrations. See [[regular fibration]]. =-- Cartesian equipments satisfying these two conditions are called _regular equipments_, and the 2-category of them is equivalent to that of regular fibrations. ### Tabulation and comprehension Recall from [[nlab:comprehension|here]] that if $E$ is a bifibration over $B$ such that the fibres $E X$ have terminal objects $T_X$, then $E$ _has comprehension_ if each image functor $im t = t_! T_Y \colon B/X \to E X$ has a right adjoint $P \mapsto \{P\} \colon E X \to B/X$ called _extension_. Say that comprehension is _full_ if the extension functors are all fully faithful. In the presence of full comprehension, we can show that for any predicate $P$ in $E X$ there is an equivalence $$ E \{P\} \simeq E X / P $$ This is well known in the case of the fibration $C \mapsto [C^{op}, Set]$ given at [[nlab:comprehension]], where the extension of a presheaf is its category of elements. We can view an equipment as a kind of double category, of course, and in that case we define the _tabulation_ of a morphism $R \colon X ⇸ Y$ to be an object $\{R\}$ together with a cell $$ \array{ \{R\} & \overset{1}{\to} & \{R\} \\ \mathllap{i}\downarrow & \Downarrow & \downarrow \mathrlap{j} \\ Y & \underset{R}{\to} & X } $$ that is universal as such, meaning that any other cell from the identity on some $Z$ to $R$, with vertical boundaries $f$ and $g$, say, is given by composing this one with (the identity cell on) a unique vertical morphism $Z \to \{R\}$. We'll say that an equipment _has tabulation_ if every horizontal morphism has a tabulation, and that these are _full_ if the mates $j_\bullet i^\bullet \to R$ of the universal cells are invertible. The point of using the same notation as for comprehension is then that a regular fibration $E$ has (full) comprehension if and only if $Matr(E)$ has (full) tabulation. Recall that if $G$ is a comonad in a bicategory, then its [[nlab:Eilenberg--Moore object]] is, if it exists, the object that represents left $G$-comodules. For an equipment, we say that an object is the EM object of $G$ if this property holds, and continues to hold when the functors involved are restricted to tight/vertical/representable maps. That's equally to ask that the universal $X ⇸ X^G$ be tight and that composition with it preserve and detect tightness. We'll say that an object is the EM object of $G$ _with respect to tight maps_ if the representation property only holds for tight maps. We can link this notion with the previous two by means of the following result: a regular equipment has tabulation if and only if every comonad has an EM object with respect to tight maps. Moreover, these are genuine EM objects if and only if the corresponding tabulations are full. ### The effective topos There are two quite different ways to construct the effective topos: we start with the Kleene algebra $(\mathbb{N}, \cdot)$ of partial recursive functions, and then 1. construct the _effective tripos_: the hyperdoctrine $\mathbf{ET}$ over $Set$ whose predicates over $X$ are $\mathbb{N}$-valued sets $X \to P\mathbb{N}$, ordered by $\phi \leq \psi$ if there exists a partial recursive function $\Phi$ such that for any $x \in X$ and $n \in \phi x$, $\Phi n$ is defined and contained in $\psi x$. The effective topos is category of _partial equivalence relations_ in $\mathbf{ET}$; or 1. construct the regular category $Asm$ of _assemblies_ over $\mathbb{N}$: the full subcategory of the total category $\int \mathbf{ET}$ on the $\mathbb{N}$-sets $\phi$ such that each $\phi x$ is non-empty, then take the [[nlab:exact completion]] of this. #### The category of pers Let $\mathbf{E} \to \mathbf{B}$ be an ordered [[regular fibration]]. A partial equivalence relation over the type $X \in \mathbf{B}$ is relation $R$ on $X$ that is symmetric and transitive: $$ \begin{aligned} R(x_1, x_2) & \Rightarrow R(x_2, x_1) \\ R(x_1, x_2), R(x_2, x_3) & \Rightarrow R(x_1, x_3) \end{aligned} $$ A morphism $(R, X) \to (S, Y)$ of pers is a relation $F \colon X, Y$ that satisfies $$ \begin{aligned} F(x,y) & \Rightarrow R(x,x) \wedge S(y,y) \\ F(x_1,y_1) \wedge R(x_1, x_2) \wedge S(y_1, y_2) & \Rightarrow F(x_2,y_2) \\ F(x,y_1) \wedge F(x,y_2) & \Rightarrow S(y_1,y_2) \\ R(x,x) & \Rightarrow \exists \upsilon . F(x, \upsilon) \end{aligned} $$ These form a category $Per(\mathbf{E})$. The effective topos is $Per(\mathbf{ET})$. #### The exact completion The category $Asm$ of assemblies is regular, so the allegory $Rel(Asm)$ is unitary and tabular. Its _effective completion_ is the splitting of equivalences $Rel(Asm)[\check{\mathrm{eqv}}]$: an equivalence is a symmetric monad, and these are the objects of the splitting, while a morphism is a [[nlab:module]]. The exact completion of $Asm$ is the category of maps in this allegory. #### Allegories vs. bicategories of relations A unitary pre-tabular allegory is the same thing as a [[nlab:bicategory of relations]]. This extends to an equivalence of 2-categories. A bicategory of relations, in turn, is a regular equipment that is both locally ordered and chordate (all maps are tight). The following two results then explain what $\mathbf{ET}$ and $Asm$ have to do with each other: * The full sub-bicategory of $Rel(Asm)$ on the constant assemblies is equivalent to $Matr(\mathbf{ET})$. * $Rel(Asm)$ is equivalent to the splitting $Matr(\mathbf{ET})[\check{\mathrm{crf}}]$ of the coreflexive morphisms in $Matr(\mathbf{ET})$. From the results of the previous section, the coreflexive splitting of a unitary pre-tabular allegory is both the tabular completion and the co-Eilenberg--Moore completion of that allegory considered as a cartesian equipment, and also the comprehensive completion of the corresponding regular fibration.