Finn Lawler thesis outline (Rev #8)

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 BiprofBiprof 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 BiprofBiprof 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:

The tricategory BiprofBiprof

We want to define the tricategory BiProfBiProf of bicategories and profunctors; we need to know what the following things are:

  1. 2-extranatural transformation
  2. 2-end
  3. free 2-cocompletion

and then we define BiProfBiProf as 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 BiprofBiprof, and an equipment functor to be a (representable) monad (op-)morphism. The existence of Kleisli objects in BiprofBiprof ensures that these definitions recover those of Wood in Wood82 and Wood85. They also have a clear relationship to some of the later ideas in CKVW.

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 strict 2-category of 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 CartEqtCartEqt. 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()Map(\mathcal{B}) \to \mathcal{B} is a cartesian equipment.

As in Shulman08, from a regular fibration EE over some category BB we can construct a cartesian equipment Matr(E)Matr(E) (of ‘matrices’ in EE): its objects are those of BB, its vertical/tight maps are the morphisms of BB and the category of horizontal maps and (globular) cells from bb to bb' is E(b×b)E(b \times b'). The important point now is that EMatr(E)E \mapsto Matr(E) is a fully faithful functor RegFibCartEqtRegFib \to CartEqt.

If BB \to \mathcal{B} is a cartesian equipment, then Pred()=( ,1)Pred(\mathcal{B}) = \mathcal{B}(-_\bullet, \mathbf{1}) is a bifibration, where f f_\bullet is the morphism in \mathcal{B} arising from a morphism ff in BB, and 1\mathbf{1} is the terminal object of BB. 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 ET\mathbf{ET} over SetSet whose predicates over XX are \mathbb{N}-valued sets XPX \to P\mathbb{N}, ordered by ϕψ\phi \leq \psi if there exists a partial recursive function Φ\Phi such that for any xXx \in X and nϕxn \in \phi x, Φn\Phi n is defined and contained in ψx\psi x. The effective topos is category of partial equivalence relations in ET\mathbf{ET}; or

  2. construct the regular category AsmAsm of assemblies over \mathbb{N}: the full subcategory of the total category ET\int \mathbf{ET} on the \mathbb{N}-sets ϕ\phi such that each ϕx\phi x is non-empty, then take the exact completion of this.

The category of pers

Let EB\mathbf{E} \to \mathbf{B} be an ordered regular fibration. A partial equivalence relation over the type XBX \in \mathbf{B} is relation RR on XX that is symmetric and transitive:

R(x 1,x 2) R(x 2,x 1) R(x 1,x 2),R(x 2,x 3) R(x 1,x 3) \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)(S,Y)(R, X) \to (S, Y) of pers is a relation F:X,YF \colon X, Y that satisfies

F(x,y) R(x,x)S(y,y) F(x 1,y 1)R(x 1,x 2)S(y 1,y 2) F(x 2,y 2) F(x,y 1)F(x,y 2) S(y 1,y 2) R(x,x) υ.F(x,υ) \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(E)Per(\mathbf{E}). The effective topos is Per(ET)Per(\mathbf{ET}).

The exact completion

The category AsmAsm of assemblies is regular, so the allegory Rel(Asm)Rel(Asm) is unitary and tabular. Its effective completion is the splitting of equivalences Rel(Asm)[eqvˇ]Rel(Asm)[\check{\mathrm{eqv}}]: an equivalence is a symmetric monad, and these are the objects of the splitting, while a morphism is a module. The exact completion of AsmAsm is the category of maps in this allegory.

Allegories vs. bicategories of relations

A unitary pre-tabular allegory is the same thing as a 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).

Proposition

The full sub-bicategory of Rel(Asm)Rel(Asm) on the constant assemblies is equivalent to Matr(ET)Matr(\mathbf{ET}).

Proposition

Rel(Asm)Rel(Asm) is equivalent to the splitting Matr(ET)[crfˇ]Matr(\mathbf{ET})[\check{\mathrm{crf}}] of the coreflexive morphisms in Matr(ET)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.

Revision on January 20, 2014 at 11:22:02 by Finn Lawler?. See the history of this page for a list of all contributions to it.