@ Christopher

You said

> I think you just systematically replace Bool with V (, and replace an equality with an equivalence, I think).

>

> > Suppose \\(X\\) and \\(Y\\) are \\(\mathcal{V}\\)-categories.

>>

>> **Puzzle 173V.** Suppose \\(f : X \to Y \\) is an \\(\mathcal{V}\\)-functor from \\(X\\) to \\(Y\\). Prove that there is a \\(\mathcal{V}\\)-profunctor \\(\Phi : X \nrightarrow Y\\) given by \\(\Phi(x,y) = Hom(f(x),\,y) \\). (i.e. that \\(\Phi\\) is a valid \\(\mathcal{V}\\)-profunctor)

>>

>> **Puzzle 174.** Suppose \\(g: Y \to X \\) is a \\(\mathcal{V}\\)-functor from \\(Y\\) to \\(X\\). Prove that there is a \\(\mathcal{V}\\)-profunctor \\(\Psi : X \nrightarrow Y\\) given by \\(\Psi(x,y) = Hom(x,\,g(y))\\).

>>

>> **Puzzle 175.** Suppose \\(f : X \to Y\\) and \\(g : Y \to X\\) are \\(\mathcal{V}\\)-functors, and use them to build \\(\mathcal{V}\\)-profunctor \\(\Phi\\) and \\(\Psi\\). When is \\(\Phi \equiv \Psi\\)?

I think you meant to address Anindya, not me.

My answer to this puzzle differs from yours. We aren't in ordinary category theory so we don't have \\(\mathrm{Hom}\\) at our disposal.

We do have \\(\mathcal{X}\\) and \\(\mathcal{Y}\\), which are like \\(\mathrm{Hom}\\)-sets, so I used those.

Moreover I assumed \\(\mathcal{V}\\) was closed and commutative so I could work with \\(\multimap\\), because otherwise I don't know how to make \\(\Phi\\) into a \\(\mathcal{V}\\)-profunctor.

But I have been playing around with a puzzle of my own: How do we define \\(\mathcal{V}\\)-profunctor composition? Can we make \\(\multimap\\) into a \\(\mathcal{V}\\)-profunctor? What happens if we compose with \\(\multimap\\)?

You said

> I think you just systematically replace Bool with V (, and replace an equality with an equivalence, I think).

>

> > Suppose \\(X\\) and \\(Y\\) are \\(\mathcal{V}\\)-categories.

>>

>> **Puzzle 173V.** Suppose \\(f : X \to Y \\) is an \\(\mathcal{V}\\)-functor from \\(X\\) to \\(Y\\). Prove that there is a \\(\mathcal{V}\\)-profunctor \\(\Phi : X \nrightarrow Y\\) given by \\(\Phi(x,y) = Hom(f(x),\,y) \\). (i.e. that \\(\Phi\\) is a valid \\(\mathcal{V}\\)-profunctor)

>>

>> **Puzzle 174.** Suppose \\(g: Y \to X \\) is a \\(\mathcal{V}\\)-functor from \\(Y\\) to \\(X\\). Prove that there is a \\(\mathcal{V}\\)-profunctor \\(\Psi : X \nrightarrow Y\\) given by \\(\Psi(x,y) = Hom(x,\,g(y))\\).

>>

>> **Puzzle 175.** Suppose \\(f : X \to Y\\) and \\(g : Y \to X\\) are \\(\mathcal{V}\\)-functors, and use them to build \\(\mathcal{V}\\)-profunctor \\(\Phi\\) and \\(\Psi\\). When is \\(\Phi \equiv \Psi\\)?

I think you meant to address Anindya, not me.

My answer to this puzzle differs from yours. We aren't in ordinary category theory so we don't have \\(\mathrm{Hom}\\) at our disposal.

We do have \\(\mathcal{X}\\) and \\(\mathcal{Y}\\), which are like \\(\mathrm{Hom}\\)-sets, so I used those.

Moreover I assumed \\(\mathcal{V}\\) was closed and commutative so I could work with \\(\multimap\\), because otherwise I don't know how to make \\(\Phi\\) into a \\(\mathcal{V}\\)-profunctor.

But I have been playing around with a puzzle of my own: How do we define \\(\mathcal{V}\\)-profunctor composition? Can we make \\(\multimap\\) into a \\(\mathcal{V}\\)-profunctor? What happens if we compose with \\(\multimap\\)?