To define the tricategory of biprofunctors, we need to know that is the free 2-cocompletion of . Then can be defined as having objects bicategories and hom-bicategories the strict 2-categories of cocontinuous pseudofunctors .
Given and , their composite corresponds to the pseudofunctor , the colimit of weighted by . Using the bicategorical co-Yoneda lemma and a couple of other tricks from Kelly section 3.3, we can write this as
showing that the composite of profunctors is indeed a ‘coend’ .
The co-Yoneda lemma then shows that if and are functors, and is a profunctor, then
If is taken as a functor , then the corresponding cocontinuous functor is its left Kan extension along the Yoneda embedding, which by the usual nerve and realization business has a right adjoint given by the pullback-along- functor . By the co-Yoneda lemma this latter is , so that the right adjoint of is equivalently . Hence in
as in .
Suppose is a pseudomonad in . Its Kleisli object is the bicategory with objects those of and hom-categories , with composition defined using the multiplication of . The unit of supplies a functor that is the identity on objects, and clearly .
The statement that is the Kleisli object of is the statement that is the universal right -module (or right -module).
We have as before the adjunction , and precomposition gives an adjunction between and , with left adjoint . Then is equivalent to the category of algebras for the monad induced by this adjunction, so there is a comparison functor , given by composition with the right -module . This comparison functor is an equivalence if the right adjoint is monadic in the sense of LMV, that is if it preserves -split codescent objects and reflects adjoint equivalences. has local colimits, which because composition is given by coends are stable under composition on both sides, so has, and preserves, the required codescent objects. Suppose is a transformation; then because is the identity on objects, the components of are exactly the components of , and so if the latter are all equivalences then so are the former. Hence is monadic, and .