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.

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