Hey Michael,

I think there might be some errors in your proof:

> We are given:
> $\Phi : Ob(\mathcal{X^{op}} \times \mathcal{Y}) \rightarrow Ob(\mathcal{V})$
> $\Psi : Ob(\mathcal{Y^{op}} \times \mathcal{Z}) \rightarrow Ob(\mathcal{V})$
>
> First we compose the two:
>
> $\Psi\Phi : Ob(\mathcal{Y^{op}} \times \mathcal{Z}) \rightarrow Ob(\mathcal{X^{op}} \times \mathcal{Y}) \rightarrow Ob(\mathcal{V})$

I don't think composition works this way.

We can [flip](https://hackage.haskell.org/package/base-4.11.1.0/docs/Prelude.html#v:flip) the order of arguments in a function and [curry](https://hackage.haskell.org/package/base-4.11.1.0/docs/Prelude.html#v:curry) them as you say.

But I don't see how we can apply transitivity in the following step:

> $\Psi\Phi : \mathcal{Z^{op}} \rightarrow \mathcal{Y} \rightarrow \mathcal{Y^{op}} \rightarrow \mathcal{X} \rightarrow Ob(\mathcal{V})$
>
> By transitivity:
>
>$\Psi\Phi : \mathcal{Z^{op}} \rightarrow \mathcal{X} \rightarrow Ob(\mathcal{V})$

Others may correct me, but I don't think we have to work very hard to prove \$$\Psi\Phi: Ob(\mathcal{X^{op}} \times \mathcal{Z}) \rightarrow Ob(\mathcal{V})\$$.

We already know the action of \$$\Psi\Phi\$$ on objects: \$$(x,z) \mapsto \bigvee_{y \in Y} \Phi(x,y) \otimes \Psi(y,z)\$$. If we were in a programming language, like Coq, then the computer could infer this mapping has the type \$$\Psi\Phi \colon \mathcal{X}^{\text{op}} \times \mathcal{Y} \to \mathcal{V} \$$ for us.