John wrote:

>> **Lemma.** For any \\(\mathcal{V}\\)-enriched category \\(\mathcal{X}\\), the \\(\mathcal{V}\\)-enriched functor \\( \mathrm{hom} \colon \mathcal{X}^{\text{op}} \times \mathcal{X} \to \mathcal{V} \\), defined by

>> \[ \mathrm{hom}(x,x') = \mathcal{X}(x,x') ,\]

>> corresponds to a \\(\mathcal{V}\\)-enriched profunctor

>> \[ 1_{\mathcal{X}} \colon \mathcal{X} \nrightarrow \mathcal{X} \]

>> that serves as an identity for composition.

Based on Yoav's comment, I think we can say further that:

\[\mathrm{hom}\_{\mathcal{X}} \otimes \mathrm{hom}\_{\mathcal{Y}} = \mathrm{hom}\_{\mathcal{X} \times \mathcal{Y}} \]

Perhaps we can also think about **Puzzle 209** from the perspective of companions and conjoints.

One way between \\(\mathcal{V}\\)-enriched categories form a category is via composition. Every \\(\mathcal{V}\\)-category has a identity functor that leaves the objects alone and \\(F \circ G (x) = F(G(x))\\) is associative and obeys the \\(\mathcal{V}\\)-laws.

Let \\(I\_{\mathcal{X}}\\) denote the identity functor for \\(\mathcal{X}\\), then we have:

\[ \hat{I}\_{\mathcal{X}} = \check{I}\_{\mathcal{X}} = \mathrm{hom}\_{\mathcal{X}} \]

Moreover, for \\(\mathbf{Bool}\\)-categories in particular, we know how to construct products. We can lift this into product functors with \\((F\times G)(x,y) := (F(x),G(y))\\). In the special case of identity functors, we have:

\[

\begin{align}

\widehat{(I\_{\mathcal{X}} \times I\_{\mathcal{Y}})} & = \hat{I}\_{\mathcal{X}} \otimes \hat{I}\_{\mathcal{Y}} \\\\

\overline{(I\_{\mathcal{X}} \times I\_{\mathcal{Y}})}& = \check{I}\_{\mathcal{X}} \otimes \check{I}\_{\mathcal{Y}} \\\\

\end{align}

\]

Here I am using \\(\overline{(I\_{\mathcal{X}} \times I\_{\mathcal{Y}})}\\) because mathjax doesn't support `\widecheck`.

This sort of leads me to wonder if we can generalize the above as a special case of two more general rules:

1. Is \\(\hat{F} \otimes \hat{G} = \widehat{F \times G}\\)?

2. Is \\(\check{F} \otimes \check{G} = \overline{F \times G}\\)?

Moreover, thinking about Puzzle 207, I have been wondering:

3. Is \\(\hat{F} \hat{G} = \widehat{F \circ G}\\)?

4. Is \\(\check{F} \check{G} = \overline{F \circ G}\\)?

I think the answer to those two questions is *yes* but I don't quite know...

>> **Lemma.** For any \\(\mathcal{V}\\)-enriched category \\(\mathcal{X}\\), the \\(\mathcal{V}\\)-enriched functor \\( \mathrm{hom} \colon \mathcal{X}^{\text{op}} \times \mathcal{X} \to \mathcal{V} \\), defined by

>> \[ \mathrm{hom}(x,x') = \mathcal{X}(x,x') ,\]

>> corresponds to a \\(\mathcal{V}\\)-enriched profunctor

>> \[ 1_{\mathcal{X}} \colon \mathcal{X} \nrightarrow \mathcal{X} \]

>> that serves as an identity for composition.

Based on Yoav's comment, I think we can say further that:

\[\mathrm{hom}\_{\mathcal{X}} \otimes \mathrm{hom}\_{\mathcal{Y}} = \mathrm{hom}\_{\mathcal{X} \times \mathcal{Y}} \]

Perhaps we can also think about **Puzzle 209** from the perspective of companions and conjoints.

One way between \\(\mathcal{V}\\)-enriched categories form a category is via composition. Every \\(\mathcal{V}\\)-category has a identity functor that leaves the objects alone and \\(F \circ G (x) = F(G(x))\\) is associative and obeys the \\(\mathcal{V}\\)-laws.

Let \\(I\_{\mathcal{X}}\\) denote the identity functor for \\(\mathcal{X}\\), then we have:

\[ \hat{I}\_{\mathcal{X}} = \check{I}\_{\mathcal{X}} = \mathrm{hom}\_{\mathcal{X}} \]

Moreover, for \\(\mathbf{Bool}\\)-categories in particular, we know how to construct products. We can lift this into product functors with \\((F\times G)(x,y) := (F(x),G(y))\\). In the special case of identity functors, we have:

\[

\begin{align}

\widehat{(I\_{\mathcal{X}} \times I\_{\mathcal{Y}})} & = \hat{I}\_{\mathcal{X}} \otimes \hat{I}\_{\mathcal{Y}} \\\\

\overline{(I\_{\mathcal{X}} \times I\_{\mathcal{Y}})}& = \check{I}\_{\mathcal{X}} \otimes \check{I}\_{\mathcal{Y}} \\\\

\end{align}

\]

Here I am using \\(\overline{(I\_{\mathcal{X}} \times I\_{\mathcal{Y}})}\\) because mathjax doesn't support `\widecheck`.

This sort of leads me to wonder if we can generalize the above as a special case of two more general rules:

1. Is \\(\hat{F} \otimes \hat{G} = \widehat{F \times G}\\)?

2. Is \\(\check{F} \otimes \check{G} = \overline{F \times G}\\)?

Moreover, thinking about Puzzle 207, I have been wondering:

3. Is \\(\hat{F} \hat{G} = \widehat{F \circ G}\\)?

4. Is \\(\check{F} \check{G} = \overline{F \circ G}\\)?

I think the answer to those two questions is *yes* but I don't quite know...