Unwinding the Statement
Let $(\mathsf{Sets},\otimes _{\mathsf{Sets}},[-_{1},-_{2}]_{\mathsf{Sets}},\mathbb {1}_{\mathsf{Sets}},\lambda ',\rho ',\sigma ')$ be a closed symmetric monoidal category satisfying Item 1 and Item 2. We need to show that the identity functor
\[ \operatorname {\mathrm{id}}_{\mathsf{Sets}}\colon \mathsf{Sets}\to \mathsf{Sets} \]
admits a unique closed symmetric monoidal functor structure
\[ \begin{array}{cccc} \phantom{\operatorname {\mathrm{id}}^{\otimes }_{\mathsf{Sets}}}\mathllap {\operatorname {\mathrm{id}}^{\otimes }_{\mathsf{Sets}}} \colon \mkern -10mu & A\otimes _{\mathsf{Sets}}B \mkern -10mu& {}\mathbin {\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }}& \mkern -10mu{}A\times B,\\ \phantom{\operatorname {\mathrm{id}}^{\otimes }_{\mathsf{Sets}}}\mathllap {\operatorname {\mathrm{id}}^{\operatorname {\mathrm{Hom}}}_{\mathsf{Sets}}} \colon \mkern -10mu & [A,B]_{\mathsf{Sets}} \mkern -10mu& {}\mathbin {\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }}& \mkern -10mu{}\mathsf{Sets}(A,B),\\ \phantom{\operatorname {\mathrm{id}}^{\otimes }_{\mathsf{Sets}}}\mathllap {\operatorname {\mathrm{id}}^{\otimes }_{\mathbb {1}|\mathsf{Sets}}} \colon \mkern -10mu & \mathbb {1}_{\mathsf{Sets}} \mkern -10mu& {}\mathbin {\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }}& \mkern -10mu{}\mathrm{pt}, \end{array} \]
making it into a symmetric monoidal strongly closed isomorphism of categories from $\left(\phantom{\mathrlap {\lambda '}}\mathsf{Sets}\right.$, $\otimes _{\mathsf{Sets}}$, $[-_{1},-_{2}]_{\mathsf{Sets}}$, $\mathbb {1}_{\mathsf{Sets}}$, $\lambda '$, $\rho '$, $\left.\sigma '\right)$ to the closed symmetric monoidal category $\left(\phantom{\mathrlap {\lambda ^{\mathsf{Sets}}}}\mathsf{Sets}\right.$, $\times $, $\mathsf{Sets}(-_{1},-_{2})$, $\mathbb {1}_{\mathsf{Sets}}$, $\lambda ^{\mathsf{Sets}}$, $\rho ^{\mathsf{Sets}}$, $\left.\sigma ^{\mathsf{Sets}}\right)$ of Proposition 5.1.9.1.1.
Constructing an Isomorphism $[-_{1},-_{2}]_{\mathsf{Sets}}\cong \mathsf{Sets}(-_{1},-_{2})$
By 
, we have a natural isomorphism
\[ \mathsf{Sets}(\mathrm{pt},[-_{1},-_{2}]_{\mathsf{Sets}})\cong \mathsf{Sets}(-_{1},-_{2}). \]
By Chapter 4: Constructions With Sets, Item 3 of Proposition 4.3.5.1.2, we also have a natural isomorphism
\[ \mathsf{Sets}(\mathrm{pt},[-_{1},-_{2}]_{\mathsf{Sets}})\cong [-_{1},-_{2}]_{\mathsf{Sets}}. \]
Composing both natural isomorphisms, we obtain a natural isomorphism
\[ \mathsf{Sets}(-_{1},-_{2})\cong [-_{1},-_{2}]_{\mathsf{Sets}}. \]
Given $A,B\in \operatorname {\mathrm{Obj}}(\mathsf{Sets})$, we will write
\[ \operatorname {\mathrm{id}}^{\operatorname {\mathrm{Hom}}}_{A,B}\colon \mathsf{Sets}(A,B)\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }[A,B]_{\mathsf{Sets}} \]
for the component of this isomorphism at $(A,B)$.
Constructing an Isomorphism $\mathord {\otimes _{\mathsf{Sets}}}\cong \mathord {\times }$
Since $\otimes _{\mathsf{Sets}}$ is adjoint in each variable to $[-_{1},-_{2}]_{\mathsf{Sets}}$ by assumption and $\times $ is adjoint in each variable to $\mathsf{Sets}(-_{1},-_{2})$ by Chapter 4: Constructions With Sets, Item 2 of Proposition 4.3.5.1.2, uniqueness of adjoints () gives us natural isomorphisms
\begin{align*} A\otimes _{\mathsf{Sets}}- & \cong A\times -,\\ -\otimes _{\mathsf{Sets}}B & \cong B\times -. \end{align*}
By , we then have $\mathord {\otimes _{\mathsf{Sets}}}\cong \mathord {\times }$. We will write
\[ \operatorname {\mathrm{id}}^{\otimes }_{\mathsf{Sets}|A,B}\colon A\otimes _{\mathsf{Sets}}B\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }A\times B \]
for the component of this isomorphism at $(A,B)$.
Alternative Construction of an Isomorphism $\mathord {\otimes _{\mathsf{Sets}}}\cong \mathord {\times }$
Alternatively, we may construct a natural isomorphism $\mathord {\otimes _{\mathsf{Sets}}}\cong \mathord {\times }$ as follows:
-
1.
Let $A\in \operatorname {\mathrm{Obj}}(\mathsf{Sets})$.
-
2.
Since $\otimes _{\mathsf{Sets}}$ is part of a closed monoidal structure, it preserves colimits in each variable by .
-
3.
Since $A\cong \mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}_{a\in A}\mathrm{pt}$ and $\otimes _{\mathsf{Sets}}$ preserves colimits in each variable, we have
\begin{align*} A\otimes _{\mathsf{Sets}}B & \cong (\coprod _{a\in A}\mathrm{pt})\otimes _{\mathsf{Sets}}B\\ & \cong \coprod _{a\in A}(\mathrm{pt}\otimes _{\mathsf{Sets}}B)\\ & \cong \coprod _{a\in A}B\\ & \cong A\times B, \end{align*}
naturally in $B\in \operatorname {\mathrm{Obj}}(\mathsf{Sets})$, where we have used that $\mathrm{pt}$ is the monoidal unit for $\otimes _{\mathsf{Sets}}$. Thus $A\otimes _{\mathsf{Sets}}-\cong A\times -$ for each $A\in \operatorname {\mathrm{Obj}}(\mathsf{Sets})$.
-
4.
Similarly, $-\otimes _{\mathsf{Sets}}B\cong -\times B$ for each $B\in \operatorname {\mathrm{Obj}}(\mathsf{Sets})$.
-
5.
By , we then have $\mathord {\otimes _{\mathsf{Sets}}}\cong \mathord {\times }$.
Below, we’ll show that if a natural isomorphism $\mathord {\otimes _{\mathsf{Sets}}}\cong \mathord {\times }$ exists, then it must be unique. This will show that the isomorphism constructed above is equal to the isomorphism $\operatorname {\mathrm{id}}^{\otimes }_{\mathsf{Sets}|A,B}\colon A\otimes _{\mathsf{Sets}}B\to A\times B$ from before.
Constructing an Isomorphism $\operatorname {\mathrm{id}}^{\otimes }_{\mathbb {1}}\colon \mathbb {1}_{\mathsf{Sets}}\to \mathrm{pt}$
We define an isomorphism $\operatorname {\mathrm{id}}^{\otimes }_{\mathbb {1}}\colon \mathbb {1}_{\mathsf{Sets}}\to \mathrm{pt}$ as the composition
\[ \mathbb {1}_{\mathsf{Sets}}\overset {\rho ^{\mathsf{Sets},-1}_{\mathbb {1}_{\mathsf{Sets}}}}{\underset {\scriptstyle \mathord {\sim }}{\dashrightarrow }}\mathbb {1}_{\mathsf{Sets}}\times \mathrm{pt}\overset {\operatorname {\mathrm{id}}^{\otimes }_{\mathsf{Sets}|\mathbb {1}_{\mathsf{Sets}}}}{\underset {\scriptstyle \mathord {\sim }}{\dashrightarrow }}\mathbb {1}_{\mathsf{Sets}}\otimes _{\mathsf{Sets}}\mathrm{pt}\overset {\lambda '_{\mathrm{pt}}}{\underset {\scriptstyle \mathord {\sim }}{\dashrightarrow }}\mathrm{pt} \]
in $\mathsf{Sets}$.
Monoidal Left Unity of the Isomorphism $\mathord {\otimes _{\mathsf{Sets}}}\cong \mathord {\times }$
We have to show that the diagram commutes. First, note that the diagram corresponding to the case $A=\mathrm{pt}$, commutes by the terminality of $\mathrm{pt}$ (Chapter 4: Constructions With Sets, Construction 4.1.1.1.2). Since this diagram commutes, so does the diagram Now, let $A\in \operatorname {\mathrm{Obj}}(\mathsf{Sets})$, let $a\in A$, and consider the diagram Since:
-
•
Subdiagram $(5)$ commutes by the naturality of $\lambda ^{\prime ,-1}$.
-
•
Subdiagram $(\dagger )$ commutes, as proved above.
-
•
Subdiagram $(4)$ commutes by the naturality of $\operatorname {\mathrm{id}}^{\otimes ,-1}_{\mathbb {1}|\mathsf{Sets}}$.
-
•
Subdiagram $(1)$ commutes by the naturality of $\operatorname {\mathrm{id}}^{\otimes ,-1}_{\mathsf{Sets}}$.
-
•
Subdiagram $(3)$ commutes by the naturality of $\lambda ^{\mathsf{Sets},-1}$.
it follows that the diagram
Here’s a step-by-step showcase of this argument:
\begin{align*} \lambda ^{\prime ,-1}_{A}(a) & = [\lambda ^{\prime ,-1}_{A}\circ [a]](\star )\\ & = [(\operatorname {\mathrm{id}}^{\otimes ,-1}_{\mathbb {1}|\mathsf{Sets}}\times \operatorname {\mathrm{id}}_{A})\circ \operatorname {\mathrm{id}}^{\otimes ,-1}_{\mathsf{Sets}|\mathrm{pt},A}\circ \lambda ^{\mathsf{Sets},-1}_{A}\circ [a]](\star )\\ & = [(\operatorname {\mathrm{id}}^{\otimes ,-1}_{\mathbb {1}|\mathsf{Sets}}\times \operatorname {\mathrm{id}}_{A})\circ \operatorname {\mathrm{id}}^{\otimes ,-1}_{\mathsf{Sets}|\mathrm{pt},A}\circ \lambda ^{\mathsf{Sets},-1}_{A}](a) \end{align*}
for each $a\in A$, and thus we have
\[ \lambda ^{\prime ,-1}_{A}=(\operatorname {\mathrm{id}}^{\otimes ,-1}_{\mathbb {1}|\mathsf{Sets}}\times \operatorname {\mathrm{id}}_{A})\circ \operatorname {\mathrm{id}}^{\otimes ,-1}_{\mathsf{Sets}|\mathrm{pt},A}\circ \lambda ^{\mathsf{Sets},-1}_{A}. \]
Taking inverses then gives
\[ \lambda ^{\prime }_{A}=\lambda ^{\mathsf{Sets}}_{A}\circ \operatorname {\mathrm{id}}^{\otimes }_{\mathsf{Sets}|\mathrm{pt},A}\circ (\operatorname {\mathrm{id}}^{\otimes }_{\mathbb {1}|\mathsf{Sets}}\times \operatorname {\mathrm{id}}_{A}), \]
showing that the diagram
indeed commutes.
Monoidal Right Unity of the Isomorphism $\mathord {\otimes _{\mathsf{Sets}}}\cong \mathord {\times }$
We can use the same argument we used to prove the monoidal left unity of the isomorphism $\mathord {\otimes _{\mathsf{Sets}}}\cong \mathord {\times }$ above. For completeness, we repeat it below.
We have to show that the diagram
commutes. First, note that the diagram corresponding to the case $A=\mathrm{pt}$, commutes by the terminality of $\mathrm{pt}$ (Chapter 4: Constructions With Sets, Construction 4.1.1.1.2). Since this diagram commutes, so does the diagram Now, let $A\in \operatorname {\mathrm{Obj}}(\mathsf{Sets})$, let $a\in A$, and consider the diagram Since:
-
•
Subdiagram $(5)$ commutes by the naturality of $\rho ^{\prime ,-1}$.
-
•
Subdiagram $(\dagger )$ commutes, as proved above.
-
•
Subdiagram $(4)$ commutes by the naturality of $\operatorname {\mathrm{id}}^{\otimes ,-1}_{\mathbb {1}|\mathsf{Sets}}$.
-
•
Subdiagram $(1)$ commutes by the naturality of $\operatorname {\mathrm{id}}^{\otimes ,-1}_{\mathsf{Sets}}$.
-
•
Subdiagram $(3)$ commutes by the naturality of $\rho ^{\mathsf{Sets},-1}$.
it follows that the diagram
Here’s a step-by-step showcase of this argument:
\begin{align*} \rho ^{\prime ,-1}_{A}(a) & = [\rho ^{\prime ,-1}_{A}\circ [a]](\star )\\ & = [(\operatorname {\mathrm{id}}_{A}\times \operatorname {\mathrm{id}}^{\otimes ,-1}_{\mathbb {1}|\mathsf{Sets}})\circ \operatorname {\mathrm{id}}^{\otimes ,-1}_{\mathsf{Sets}|\mathrm{pt},A}\circ \rho ^{\mathsf{Sets},-1}_{A}\circ [a]](\star )\\ & = [(\operatorname {\mathrm{id}}_{A}\times \operatorname {\mathrm{id}}^{\otimes ,-1}_{\mathbb {1}|\mathsf{Sets}})\circ \operatorname {\mathrm{id}}^{\otimes ,-1}_{\mathsf{Sets}|\mathrm{pt},A}\circ \rho ^{\mathsf{Sets},-1}_{A}](a) \end{align*}
for each $a\in A$, and thus we have
\[ \rho ^{\prime ,-1}_{A}=(\operatorname {\mathrm{id}}_{A}\times \operatorname {\mathrm{id}}^{\otimes ,-1}_{\mathbb {1}|\mathsf{Sets}})\circ \operatorname {\mathrm{id}}^{\otimes ,-1}_{\mathsf{Sets}|\mathrm{pt},A}\circ \rho ^{\mathsf{Sets},-1}_{A}. \]
Taking inverses then gives
\[ \rho ^{\prime }_{A}=\rho ^{\mathsf{Sets}}_{A}\circ \operatorname {\mathrm{id}}^{\otimes }_{\mathsf{Sets}|\mathrm{pt},A}\circ (\operatorname {\mathrm{id}}_{A}\times \operatorname {\mathrm{id}}^{\otimes }_{\mathbb {1}|\mathsf{Sets}}), \]
showing that the diagram
indeed commutes.
Monoidality of the Isomorphism $\mathord {\otimes _{\mathsf{Sets}}}\cong \mathord {\times }$
We have to show that the diagram commutes. First, note that the diagram commutes by the terminality of $\mathrm{pt}$ (Chapter 4: Constructions With Sets, Construction 4.1.1.1.2). Since the map $!_{\mathrm{pt}\times (\mathrm{pt}\times \mathrm{pt})}\colon \mathrm{pt}\times (\mathrm{pt}\times \mathrm{pt})\to \mathrm{pt}$ is an isomorphism (e.g. having inverse $\lambda ^{\mathsf{Sets},-1}_{\mathrm{pt}}\circ \lambda ^{\mathsf{Sets},-1}_{\mathrm{pt}}$), it follows that the diagram also commutes. Taking inverses, we see that the diagram commutes as well. Now, let $A,B,C\in \operatorname {\mathrm{Obj}}(\mathsf{Sets})$, let $a\in A$, let $b\in B$, let $c\in C$, and consider the diagram which we partition into subdiagrams as follows: Since:
-
•
Subdiagram $(1)$ commutes by the naturality of $\alpha ^{\mathsf{Sets},-1}$.
-
•
Subdiagram $(2)$ commutes by the naturality of $\operatorname {\mathrm{id}}^{\otimes ,-1}_{\mathsf{Sets}}$.
-
•
Subdiagram $(3)$ commutes by the naturality of $\operatorname {\mathrm{id}}^{\otimes ,-1}_{\mathsf{Sets}}$.
-
•
Subdiagram $(\dagger )$ commutes, as proved above.
-
•
Subdiagram $(4)$ commutes by the naturality of $\operatorname {\mathrm{id}}^{\otimes ,-1}_{\mathsf{Sets}}$.
-
•
Subdiagram $(5)$ commutes by the naturality of $\operatorname {\mathrm{id}}^{\otimes ,-1}_{\mathsf{Sets}}$.
-
•
Subdiagram $(6)$ commutes by the naturality of $\alpha ^{\prime ,-1}$.
it follows that the diagram
also commutes. We then have
\begin{align*} \left[(\operatorname {\mathrm{id}}^{\otimes ,-1}_{\mathsf{Sets}|A,B}\otimes _{\mathsf{Sets}}\operatorname {\mathrm{id}}_{C})\circ \operatorname {\mathrm{id}}^{\otimes ,-1}_{\mathsf{Sets}|A\times B,C}\right.\\ \left.{}\circ \alpha ^{\mathsf{Sets},-1}_{A,B,C}\right](a,(b,c)) & = \left[(\operatorname {\mathrm{id}}^{\otimes ,-1}_{\mathsf{Sets}|A,B}\otimes _{\mathsf{Sets}}\operatorname {\mathrm{id}}_{C})\circ \operatorname {\mathrm{id}}^{\otimes ,-1}_{\mathsf{Sets}|A\times B,C}\right.\\ & \phantom{={}} \mkern 4mu\left.{}{}\circ \alpha ^{\mathsf{Sets},-1}_{A,B,C}\circ ([a]\times ([b]\times [c]))\right](\star ,(\star ,\star ))\\ & = \left[\alpha ^{\prime ,-1}_{A,B,C}\circ (\operatorname {\mathrm{id}}_{A}\times \operatorname {\mathrm{id}}^{\otimes ,-1}_{\mathsf{Sets}|B,C})\right.\\ & \phantom{={}} \mkern 4mu\left.{}\circ \operatorname {\mathrm{id}}^{\otimes ,-1}_{\mathsf{Sets}|A,B\times C}\circ ([a]\times ([b]\times [c]))\right](\star ,(\star ,\star ))\\ & = [\alpha ^{\prime ,-1}_{A,B,C}\circ (\operatorname {\mathrm{id}}_{A}\times \operatorname {\mathrm{id}}^{\otimes ,-1}_{\mathsf{Sets}|B,C})\circ \operatorname {\mathrm{id}}^{\otimes ,-1}_{\mathsf{Sets}|A,B\times C}](a,(b,c)) \end{align*}
for each $(a,(b,c))\in A\times (B\times C)$, and thus we have Taking inverses then gives showing that the diagram indeed commutes.
Braidedness of the Isomorphism $\mathord {\otimes _{\mathsf{Sets}}}\cong \mathord {\times }$
We have to show that the diagram commutes. First, note that the diagram commutes by the terminality of $\mathrm{pt}$ (Chapter 4: Constructions With Sets, Construction 4.1.1.1.2). Since the map $!_{\mathrm{pt}\times \mathrm{pt}}\colon \mathrm{pt}\times \mathrm{pt}\to \mathrm{pt}$ is invertible (e.g. with inverse $\lambda ^{\mathsf{Sets},-1}_{\mathrm{pt}}$), the diagram also commutes. Taking inverses, we see that the diagram commutes as well. Now, let $A,B\in \operatorname {\mathrm{Obj}}(\mathsf{Sets})$, let $a\in A$, let $b\in B$, and consider the diagram which we partition into subdiagrams as follows: Since:
-
•
Subdiagram $(2)$ commutes by the naturality of $\sigma ^{\mathsf{Sets},-1}$.
-
•
Subdiagram $(5)$ commutes by the naturality of $\operatorname {\mathrm{id}}^{\otimes ,-1}$.
-
•
Subdiagram $(\dagger )$ commutes, as proved above.
-
•
Subdiagram $(4)$ commutes by the naturality of $\sigma ^{\prime ,-1}$.
-
•
Subdiagram $(1)$ commutes by the naturality of $\operatorname {\mathrm{id}}^{\otimes ,-1}$.
it follows that the diagram
commutes. We then have
\begin{align*} [\operatorname {\mathrm{id}}^{\otimes ,-1}_{\mathsf{Sets}|A,B}\circ \sigma ^{\mathsf{Sets},-1}_{A,B}](b,a) & = [\operatorname {\mathrm{id}}^{\otimes ,-1}_{\mathsf{Sets}|A,B}\circ \sigma ^{\mathsf{Sets},-1}_{A,B}\circ ([b]\times [a])](\star ,\star )\\ & = [\sigma ^{\prime ,-1}_{A,B}\circ \operatorname {\mathrm{id}}^{\otimes ,-1}_{\mathsf{Sets}|B,A}\circ ([b]\times [a])](\star ,\star )\\ & = [\sigma ^{\prime ,-1}_{A,B}\circ \operatorname {\mathrm{id}}^{\otimes ,-1}_{\mathsf{Sets}|B,A}](b,a) \end{align*}
for each $(b,a)\in B\times A$, and thus we have
\[ \operatorname {\mathrm{id}}^{\otimes ,-1}_{\mathsf{Sets}|A,B}\circ \sigma ^{\mathsf{Sets},-1}_{A,B}=\sigma ^{\prime ,-1}_{A,B}\circ \operatorname {\mathrm{id}}^{\otimes ,-1}_{\mathsf{Sets}|B,A}. \]
Taking inverses then gives
\[ \sigma ^{\mathsf{Sets}}_{A,B}\circ \operatorname {\mathrm{id}}^{\otimes }_{\mathsf{Sets}|A,B}=\operatorname {\mathrm{id}}^{\otimes }_{\mathsf{Sets}|B,A}\circ \sigma ^{\prime }_{A,B}, \]
showing that the diagram
indeed commutes.
Uniqueness of the Isomorphism $\mathord {\otimes _{\mathsf{Sets}}}\cong \mathord {\times }$
Let $\phi ,\psi \colon -_{1}\otimes _{\mathsf{Sets}}-_{2}\Rightarrow -_{1}\times -_{2}$ be natural isomorphisms. Since these isomorphisms are compatible with the unitors of $\mathsf{Sets}$ with respect to $\times $ and $\otimes $ (as shown above), we have
\begin{align*} \lambda '_{B} & = \lambda ^{\mathsf{Sets}}_{B}\circ \phi _{\mathrm{pt},B}\circ (\operatorname {\mathrm{id}}^{\otimes }_{\mathbb {1}|\mathsf{Sets}}\otimes _{\mathsf{Sets}}\operatorname {\mathrm{id}}_{Y}),\\ \lambda '_{B} & = \lambda ^{\mathsf{Sets}}_{B}\circ \psi _{\mathrm{pt},B}\circ (\operatorname {\mathrm{id}}^{\otimes }_{\mathbb {1}|\mathsf{Sets}}\otimes _{\mathsf{Sets}}\operatorname {\mathrm{id}}_{Y}). \end{align*}
Postcomposing both sides with $\lambda ^{\mathsf{Sets},-1}_{B}$ gives
\begin{align*} \lambda ^{\mathsf{Sets},-1}_{B}\circ \lambda '_{B}\circ (\operatorname {\mathrm{id}}^{\otimes ,-1}_{\mathbb {1}|\mathsf{Sets}}\otimes _{\mathsf{Sets}}\operatorname {\mathrm{id}}_{Y}) & = \phi _{\mathrm{pt},B},\\ \lambda ^{\mathsf{Sets},-1}_{B}\circ \lambda '_{B}\circ (\operatorname {\mathrm{id}}^{\otimes }_{\mathbb {1}|\mathsf{Sets}}\otimes _{\mathsf{Sets}}\operatorname {\mathrm{id}}_{Y}) & = \psi _{\mathrm{pt},B}, \end{align*}
and thus we have
\[ \phi _{\mathrm{pt},B}=\psi _{\mathrm{pt},B} \]
for each $B\in \operatorname {\mathrm{Obj}}(\mathsf{Sets})$. Now, let $a\in A$ and consider the naturality diagrams
for $\phi $ and $\psi $ with respect to the morphisms $[a]$ and $\operatorname {\mathrm{id}}_{B}$. Having shown that $\phi _{\mathrm{pt},B}=\psi _{\mathrm{pt},B}$, we have
\begin{align*} \phi _{A,B}(a,b) & = [\phi _{A,B}\circ ([a]\times \operatorname {\mathrm{id}}_{B})](\star ,b)\\ & = [([a]\otimes _{\mathsf{Sets}}\operatorname {\mathrm{id}}_{B})\circ \phi _{\mathrm{pt},B}](\star ,b)\\ & = [([a]\otimes _{\mathsf{Sets}}\operatorname {\mathrm{id}}_{B})\circ \psi _{\mathrm{pt},B}](\star ,b)\\ & = [\psi _{A,B}\circ ([a]\times \operatorname {\mathrm{id}}_{B})](\star ,b)\\ & = \psi _{A,B}(a,b) \end{align*}
for each $(a,b)\in A\times B$. Therefore we have
\[ \phi _{A,B}=\psi _{A,B} \]
for each $A,B\in \operatorname {\mathrm{Obj}}(\mathsf{Sets})$ and thus $\phi =\psi $, showing the isomorphism $\mathord {\otimes _{\mathsf{Sets}}}\cong \mathord {\times }$ to be unique.
