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- the order of arguments in a function and [`curry`](https://hackage.haskell.org/package/base- 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.