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.

Instead, we have

\[ \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\\)