My thesis has been submitted, but not examined or accepted yet, so uploading it is probably out of the question for now. But I don't think anyone will object to my reproducing the abstract here, and giving an outline of the basic ideas. # 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]] * [[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. 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 _coming soon_ ### 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 cartesian equipment that is both locally ordered and chordate (all maps are tight). +-- {: .un_prop} ###### Proposition The full sub-bicategory of $Rel(Asm)$ on the constant assemblies is equivalent to $Matr(\mathbf{ET})$. =-- +-- {: .un_prop} ###### Proposition $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.