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 _coming soon_