John -

> I seem to recall Matthew had trouble proving the composite of conjoints is the conjoint of the composite:
>
> $\check{FG} \stackrel{?}{=} \check{F} \check{G} .$
>
> I don't even know if this is true! It would seem strangely asymmetrical for this to be false.

It is asymmetrical! I don't think this is true in general.

$\check{G F} = \check{F} \check{G}$

Back in [Lecture 65](https://forum.azimuthproject.org/discussion/2299/lecture-65-chapter-4-collaborative-design/p1), you more or less wrote:

> Any \$$\mathcal{V}\$$-enriched functor \$$F: \mathcal{X} \to \mathcal{Y}\$$ gives a \$$\mathcal{V}\$$-enriched profunctor
>
> $\check{F} \colon \mathcal{Y} \nrightarrow \mathcal{X}$
>
> called the conjoint of \$$F\$$. It is defined by
>
> $\check{F} (y,x) = \mathcal{Y}(y,F(x)) .$

So let's prove \$$\check{F} \circ \check{G} = \check{G F} \$$ (this is just copy pasta from Anindya). Assume \$$F : \mathcal{X} \to \mathcal{Y}, G : \mathcal{Y} \to \mathcal{Z}\$$. Then:

\begin{align} (\check{F} \circ \check{G})(x, z) & = \bigvee_y\left(\check{G}(x, y) \otimes \check{F}(y, z)\right) \\\ & = \bigvee_y\left(\mathcal{Z}(x, G y) \otimes \mathcal{Y}(y, F z)\right) \end{align}

Setting \$$y = F z\$$, we have:

\begin{align} \bigvee_y\left(\mathcal{Z}(x, G y) \otimes \mathcal{Y}(y, F z)\right) & \geq \mathcal{Z}(x, G F z) \otimes \mathcal{Y}(F z , F z) \\\\ & \ge \mathcal{Z}(x, G F z) \otimes I \\\\ & \ge \mathcal{Z}(x, G F z) \end{align}

For any \$$y\$$ we have

\begin{align} \mathcal{Z}(x, G F z) & \geq \mathcal{Z}(x, G y) \otimes \mathcal{Z}(G y, G F z) \\\\ & \geq \mathcal{Z}(x, G y) \otimes \mathcal{Y}(y, F z) \\\\ \end{align}

Hence, because \$$\mathcal{Z}(x, G F z)\$$ is an upper bound, we have \$$\mathcal{Z}(x, G F z) \ge \bigvee_y\left(\mathcal{Z}(x, G y) \otimes \mathcal{Y}(y, F z)\right) \$$.

Putting this all together, we have

$\mathcal{Z}(x, G F z) = \bigvee_y\left(\mathcal{Z}(x, G y) \otimes \mathcal{Y}(y, F z)\right)$

Which is the same as saying \$$\check{G F}(x,z) = (\check{F} \check{G})(x,z)\$$. \$$\quad\quad \blacksquare\$$