Finn Lawler biprofunctor (Rev #1)

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)$.