@MatthewDoty

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

And then the proofs transform too IIRC.

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

And then the proofs transform too IIRC.