Finn Lawler biprofunctor (Rev #2)

Definition

If $K$ and $L$ are bicategories, then a biprofunctor $H \colon K ⇸ L$ is a pseudofunctor $\bar H \colon L^{op} \times K \to Cat$.

To define the tricategory $BiProf$ of biprofunctors, we need to know that $P K = [K^{op}, Cat]$ is the free 2-cocompletion of $K$. Then $BiProf$ can be defined as having objects bicategories $K,L,\ldots$ and hom-bicategories $\hom(K,L)$ the strict 2-categories of cocontinuous pseudofunctors $P K \to P L$.

Given $H \colon P K \to P L$ and $G \colon P L \to P M$, their composite $G H$ corresponds to the pseudofunctor $\bar{G H}(m,k) = (G H y k) m = \bar H(-, k) \star \bar G(m,-)$, the colimit of $\bar G(m,-)$ weighted by $\bar H(-,k)$. 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 $\bar{G H}$ of profunctors is indeed a ‘coend’ $\int^\ell H(\ell,-) \times G(-,\ell)$.

The co-Yoneda lemma then shows that if $F \colon K \to L$ and $G \colon J \to M$ are functors, and $H \colon L ⇸ M$ is a profunctor, then