The symmetric monoidal structure on the category $\mathsf{Sets}$ of Proposition 3.1.9.1.1 is uniquely determined by the following requirements:

  1. Existence of an Internal Hom. The product
    \[ \times \colon \mathsf{Sets}\times \mathsf{Sets}\to \mathsf{Sets} \]

    of $\mathsf{Sets}$ admits an internal Hom $\webleft [-_{1},-_{2}\webright ]_{\mathsf{Sets}}$.

  2. The Unit Object Is $\text{pt}$. We have $\mathbb {1}_{\mathsf{Sets}}=\text{pt}$.

More precisely, the full subcategory of the category $\mathcal{M}^{\mathrm{cld}}_{\mathbb {E}_{\infty }}\webleft (\mathsf{Sets}\webright )$ of spanned by the closed symmetric monoidal categories $\webleft(\phantom{\mathrlap {\lambda ^{\mathsf{Sets}}}}\mathsf{Sets}\right.$, $\otimes _{\mathsf{Sets}}$, $\webleft [-_{1},-_{2}\webright ]_{\mathsf{Sets}}$, $\mathbb {1}_{\mathsf{Sets}}$, $\lambda ^{\mathsf{Sets}}$, $\rho ^{\mathsf{Sets}}$, $\left.\sigma ^{\mathsf{Sets}}\webright)$ satisfying Item 1 and Item 2 is contractible (i.e. equivalent to the punctual category).

Unwinding the Statement
Let $\webleft (\mathsf{Sets},\otimes _{\mathsf{Sets}},\webleft [-_{1},-_{2}\webright ]_{\mathsf{Sets}},\mathbb {1}_{\mathsf{Sets}},\lambda ',\rho ',\sigma '\webright )$ be a closed symmetric monoidal category satisfying Item 1 and Item 2. We need to show that the identity functor

\[ \text{id}_{\mathsf{Sets}}\colon \mathsf{Sets}\to \mathsf{Sets} \]

admits a unique symmetric closed monoidal functor structure

\begin{gather*} \text{id}^{\otimes }_{\mathsf{Sets}} \colon A\otimes _{\mathsf{Sets}}B \overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }A\times B,\\ \text{id}^{\textup{Hom}}_{\mathsf{Sets}} \colon \webleft [A,B\webright ]_{\mathsf{Sets}} \overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }\mathsf{Sets}\webleft (A,B\webright ),\\ \text{id}^{\otimes }_{\mathbb {1}|\mathsf{Sets}} \colon \mathbb {1}_{\mathsf{Sets}} \overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }\text{pt}\end{gather*}

making it into a symmetric monoidal strongly closed isomorphism of categories from $\webleft(\phantom{\mathrlap {\lambda '}}\mathsf{Sets}\right.$, $\otimes _{\mathsf{Sets}}$, $\webleft [-_{1},-_{2}\webright ]_{\mathsf{Sets}}$, $\mathbb {1}_{\mathsf{Sets}}$, $\lambda '$, $\rho '$, $\left.\sigma '\webright)$ to the closed symmetric monoidal category $\webleft(\phantom{\mathrlap {\lambda ^{\mathsf{Sets}}}}\mathsf{Sets}\right.$, $\times $, $\mathsf{Sets}\webleft (-_{1},-_{2}\webright )$, $\mathbb {1}_{\mathsf{Sets}}$, $\lambda ^{\mathsf{Sets}}$, $\rho ^{\mathsf{Sets}}$, $\left.\sigma ^{\mathsf{Sets}}\webright)$ of $\mathsf{Sets}$ and products of Proposition 3.1.9.1.1.

Constructing an Isomorphism $\webleft [-_{1},-_{2}\webright ]_{\mathsf{Sets}}\cong \mathsf{Sets}\webleft (-_{1},-_{2}\webright )$
By , we have a natural isomorphism

\[ \mathsf{Sets}\webleft (\text{pt},\webleft [-_{1},-_{2}\webright ]_{\mathsf{Sets}}\webright )\cong \mathsf{Sets}\webleft (-_{1},-_{2}\webright ). \]

By Chapter 2: Constructions With Sets, Item 3 of Proposition 2.3.5.1.2, we also have a natural isomorphism

\[ \mathsf{Sets}\webleft (\text{pt},\webleft [-_{1},-_{2}\webright ]_{\mathsf{Sets}}\webright )\cong \webleft [-_{1},-_{2}\webright ]_{\mathsf{Sets}}. \]

Composing both natural isomorphisms, we obtain a natural isomorphism

\[ \mathsf{Sets}\webleft (-_{1},-_{2}\webright )\cong \webleft [-_{1},-_{2}\webright ]_{\mathsf{Sets}}. \]

Given $A,B\in \text{Obj}\webleft (\mathsf{Sets}\webright )$, we will write

\[ \text{id}^{\textup{Hom}}_{A,B}\colon \mathsf{Sets}\webleft (A,B\webright )\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }\webleft [A,B\webright ]_{\mathsf{Sets}} \]

for the component of this isomorphism at $\webleft (A,B\webright )$.

Constructing an Isomorphism $\mathord {\otimes _{\mathsf{Sets}}}\cong \mathord {\times }$
Since $\otimes _{\mathsf{Sets}}$ is adjoint in each variable to $\webleft [-_{1},-_{2}\webright ]_{\mathsf{Sets}}$ by assumption and $\times $ is adjoint in each variable to $\mathsf{Sets}\webleft (-_{1},-_{2}\webright )$ by Chapter 2: Constructions With Sets, Item 2 of Proposition 2.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

\[ \text{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 $\webleft (A,B\webright )$.

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 \text{Obj}\webleft (\mathsf{Sets}\webright )$.
  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}\text{pt}$ and $\otimes _{\mathsf{Sets}}$ preserves colimits in each variable, we have
    \begin{align*} A\otimes _{\mathsf{Sets}}B & \cong \webleft (\coprod _{a\in A}\text{pt}\webright )\otimes _{\mathsf{Sets}}B\\ & \cong \coprod _{a\in A}\webleft (\text{pt}\otimes _{\mathsf{Sets}}B\webright )\\ & \cong \coprod _{a\in A}B\\ & \cong A\times B, \end{align*}

    naturally in $B\in \text{Obj}\webleft (\mathsf{Sets}\webright )$, where we have used that $\text{pt}$ is the monoidal unit for $\otimes _{\mathsf{Sets}}$. Thus $A\otimes _{\mathsf{Sets}}-\cong A\times -$ for each $A\in \text{Obj}\webleft (\mathsf{Sets}\webright )$.

  4. Similarly, $-\otimes _{\mathsf{Sets}}B\cong -\times B$ for each $B\in \text{Obj}\webleft (\mathsf{Sets}\webright )$.
  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 $\text{id}^{\otimes }_{\mathsf{Sets}|A,B}\colon A\otimes _{\mathsf{Sets}}B\to A\times B$ from before.

Constructing an Isomorphism $\text{id}^{\otimes }_{\mathbb {1}}\colon \mathbb {1}_{\mathsf{Sets}}\to \text{pt}$
We define an isomorphism $\text{id}^{\otimes }_{\mathbb {1}}\colon \mathbb {1}_{\mathsf{Sets}}\to \text{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 \text{pt}\overset {\text{id}^{\otimes }_{\mathsf{Sets}|\mathbb {1}_{\mathsf{Sets}}}}{\underset {\scriptstyle \mathord {\sim }}{\dashrightarrow }}\mathbb {1}_{\mathsf{Sets}}\otimes _{\mathsf{Sets}}\text{pt}\overset {\lambda '_{\text{pt}}}{\underset {\scriptstyle \mathord {\sim }}{\dashrightarrow }}\text{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=\text{pt}$, commutes by the terminality of $\text{pt}$ (Chapter 2: Constructions With Sets, Construction 2.1.1.1.2). Since this diagram commutes, so does the diagram

Now, let $A\in \text{Obj}\webleft (\mathsf{Sets}\webright )$, 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 $\text{id}^{\otimes ,-1}_{\mathbb {1}|\mathsf{Sets}}$.
  • Subdiagram (1) commutes by the naturality of $\text{id}^{\otimes ,-1}_{\mathsf{Sets}}$.
  • Subdiagram (3) commutes by the naturality of $\lambda ^{\mathsf{Sets},-1}$.
it follows that the diagram

also commutes. Here’s an interactive step-by-step showcase of this argument:

We then have

\begin{align*} \lambda ^{\prime ,-1}_{A}\webleft (a\webright ) & = \webleft [\lambda ^{\prime ,-1}_{A}\circ \webleft [a\webright ]\webright ]\webleft (\star \webright )\\ & = \webleft [\webleft (\text{id}^{\otimes ,-1}_{\mathbb {1}|\mathsf{Sets}}\times \text{id}_{A}\webright )\circ \text{id}^{\otimes ,-1}_{\mathsf{Sets}|\text{pt},A}\circ \lambda ^{\mathsf{Sets},-1}_{A}\circ \webleft [a\webright ]\webright ]\webleft (\star \webright )\\ & = \webleft [\webleft (\text{id}^{\otimes ,-1}_{\mathbb {1}|\mathsf{Sets}}\times \text{id}_{A}\webright )\circ \text{id}^{\otimes ,-1}_{\mathsf{Sets}|\text{pt},A}\circ \lambda ^{\mathsf{Sets},-1}_{A}\webright ]\webleft (a\webright ) \end{align*}

for each $a\in A$, and thus we have

\[ \lambda ^{\prime ,-1}_{A}=\webleft (\text{id}^{\otimes ,-1}_{\mathbb {1}|\mathsf{Sets}}\times \text{id}_{A}\webright )\circ \text{id}^{\otimes ,-1}_{\mathsf{Sets}|\text{pt},A}\circ \lambda ^{\mathsf{Sets},-1}_{A}. \]

Taking inverses then gives

\[ \lambda ^{\prime }_{A}=\lambda ^{\mathsf{Sets}}_{A}\circ \text{id}^{\otimes }_{\mathsf{Sets}|\text{pt},A}\circ \webleft (\text{id}^{\otimes }_{\mathbb {1}|\mathsf{Sets}}\times \text{id}_{A}\webright ), \]

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=\text{pt}$, commutes by the terminality of $\text{pt}$ (Chapter 2: Constructions With Sets, Construction 2.1.1.1.2). Since this diagram commutes, so does the diagram

Now, let $A\in \text{Obj}\webleft (\mathsf{Sets}\webright )$, 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 $\text{id}^{\otimes ,-1}_{\mathbb {1}|\mathsf{Sets}}$.
  • Subdiagram (1) commutes by the naturality of $\text{id}^{\otimes ,-1}_{\mathsf{Sets}}$.
  • Subdiagram (3) commutes by the naturality of $\rho ^{\mathsf{Sets},-1}$.
it follows that the diagram

also commutes. Here’s an interactive step-by-step showcase of this argument:

We then have

\begin{align*} \rho ^{\prime ,-1}_{A}\webleft (a\webright ) & = \webleft [\rho ^{\prime ,-1}_{A}\circ \webleft [a\webright ]\webright ]\webleft (\star \webright )\\ & = \webleft [\webleft (\text{id}_{A}\times \text{id}^{\otimes ,-1}_{\mathbb {1}|\mathsf{Sets}}\webright )\circ \text{id}^{\otimes ,-1}_{\mathsf{Sets}|\text{pt},A}\circ \rho ^{\mathsf{Sets},-1}_{A}\circ \webleft [a\webright ]\webright ]\webleft (\star \webright )\\ & = \webleft [\webleft (\text{id}_{A}\times \text{id}^{\otimes ,-1}_{\mathbb {1}|\mathsf{Sets}}\webright )\circ \text{id}^{\otimes ,-1}_{\mathsf{Sets}|\text{pt},A}\circ \rho ^{\mathsf{Sets},-1}_{A}\webright ]\webleft (a\webright ) \end{align*}

for each $a\in A$, and thus we have

\[ \rho ^{\prime ,-1}_{A}=\webleft (\text{id}_{A}\times \text{id}^{\otimes ,-1}_{\mathbb {1}|\mathsf{Sets}}\webright )\circ \text{id}^{\otimes ,-1}_{\mathsf{Sets}|\text{pt},A}\circ \rho ^{\mathsf{Sets},-1}_{A}. \]

Taking inverses then gives

\[ \rho ^{\prime }_{A}=\rho ^{\mathsf{Sets}}_{A}\circ \text{id}^{\otimes }_{\mathsf{Sets}|\text{pt},A}\circ \webleft (\text{id}_{A}\times \text{id}^{\otimes }_{\mathbb {1}|\mathsf{Sets}}\webright ), \]

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 $\text{pt}$ (Chapter 2: Constructions With Sets, Construction 2.1.1.1.2). Since the map $!_{\text{pt}\times \webleft (\text{pt}\times \text{pt}\webright )}\colon \text{pt}\times \webleft (\text{pt}\times \text{pt}\webright )\to \text{pt}$ is an isomorphism (e.g. having inverse $\lambda ^{\mathsf{Sets},-1}_{\text{pt}}\circ \lambda ^{\mathsf{Sets},-1}_{\text{pt}}$), it follows that the diagram

also commutes. Taking inverses, we see that the diagram

commutes as well. Now, let $A\in \text{Obj}\webleft (\mathsf{Sets}\webright )$, let $a\in A$, 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 $\text{id}^{\otimes ,-1}_{\mathsf{Sets}}$.
  • Subdiagram (3) commutes by the naturality of $\text{id}^{\otimes ,-1}_{\mathsf{Sets}}$.
  • Subdiagram ($\dagger $) commutes, as proved above.
  • Subdiagram (4) commutes by the naturality of $\text{id}^{\otimes ,-1}_{\mathsf{Sets}}$.
  • Subdiagram (5) commutes by the naturality of $\text{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*} \webleft[\webleft (\text{id}^{\otimes ,-1}_{\mathsf{Sets}|A,B}\otimes _{\mathsf{Sets}}\text{id}_{C}\webright )\circ \text{id}^{\otimes ,-1}_{\mathsf{Sets}|A\times B,C}\right.\\ \left.{}\circ \alpha ^{\mathsf{Sets},-1}_{A,B,C}\webright]\webleft (a,\webleft (b,c\webright )\webright ) & = \webleft[\webleft (\text{id}^{\otimes ,-1}_{\mathsf{Sets}|A,B}\otimes _{\mathsf{Sets}}\text{id}_{C}\webright )\circ \text{id}^{\otimes ,-1}_{\mathsf{Sets}|A\times B,C}\right.\\ & \phantom{={}} \mkern 4mu\left.{}{}\circ \alpha ^{\mathsf{Sets},-1}_{A,B,C}\circ \webleft (\webleft [a\webright ]\times \webleft (\webleft [b\webright ]\times \webleft [c\webright ]\webright )\webright )\webright]\webleft (\star ,\webleft (\star ,\star \webright )\webright )\\ & = \webleft[\alpha ^{\prime ,-1}_{A,B,C}\circ \webleft (\text{id}_{A}\times \text{id}^{\otimes ,-1}_{\mathsf{Sets}|B,C}\webright )\right.\\ & \phantom{={}} \mkern 4mu\left.{}\circ \text{id}^{\otimes ,-1}_{\mathsf{Sets}|A,B\times C}\circ \webleft (\webleft [a\webright ]\times \webleft (\webleft [b\webright ]\times \webleft [c\webright ]\webright )\webright )\webright]\webleft (\star ,\webleft (\star ,\star \webright )\webright )\\ & = \webleft [\alpha ^{\prime ,-1}_{A,B,C}\circ \webleft (\text{id}_{A}\times \text{id}^{\otimes ,-1}_{\mathsf{Sets}|B,C}\webright )\circ \text{id}^{\otimes ,-1}_{\mathsf{Sets}|A,B\times C}\webright ]\webleft (a,\webleft (b,c\webright )\webright ) \end{align*}

for each $\webleft (a,\webleft (b,c\webright )\webright )\in A\times \webleft (B\times C\webright )$, and thus we have

\[ \webleft (\text{id}^{\otimes ,-1}_{\mathsf{Sets}|A,B}\otimes _{\mathsf{Sets}}\text{id}_{C}\webright )\circ \text{id}^{\otimes ,-1}_{\mathsf{Sets}|A\times B,C}\circ \alpha ^{\mathsf{Sets},-1}_{A,B,C}=\alpha ^{\prime ,-1}_{A,B,C}\circ \webleft (\text{id}_{A}\times \text{id}^{\otimes ,-1}_{\mathsf{Sets}|B,C}\webright )\circ \text{id}^{\otimes ,-1}_{\mathsf{Sets}|A,B\times C}. \]

Taking inverses then gives

\[ \alpha ^{\mathsf{Sets}}_{A,B,C}\circ \text{id}^{\otimes }_{\mathsf{Sets}|A\times B,C}\circ \webleft (\text{id}^{\otimes }_{\mathsf{Sets}|A,B}\otimes _{\mathsf{Sets}}\text{id}_{C}\webright )=\text{id}^{\otimes }_{\mathsf{Sets}|A,B\times C}\circ \webleft (\text{id}_{A}\times \text{id}^{\otimes }_{\mathsf{Sets}|B,C}\webright )\circ \alpha ^{\prime }_{A,B,C}, \]

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 $\text{pt}$ (Chapter 2: Constructions With Sets, Construction 2.1.1.1.2). Since the map $!_{\text{pt}\times \text{pt}}\colon \text{pt}\times \text{pt}\to \text{pt}$ is invertible (e.g. with inverse $\lambda ^{\mathsf{Sets},-1}_{\text{pt}}$), the diagram

also commutes. Taking inverses, we see that the diagram

commutes as well. Now, let $A\in \text{Obj}\webleft (\mathsf{Sets}\webright )$, let $a\in A$, 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 $\text{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 $\text{id}^{\otimes ,-1}$.
it follows that the diagram

commutes. We then have

\begin{align*} \webleft [\text{id}^{\otimes ,-1}_{\mathsf{Sets}|A,B}\circ \sigma ^{\mathsf{Sets},-1}_{A,B}\webright ]\webleft (b,a\webright ) & = \webleft [\text{id}^{\otimes ,-1}_{\mathsf{Sets}|A,B}\circ \sigma ^{\mathsf{Sets},-1}_{A,B}\circ \webleft (\webleft [b\webright ]\times \webleft [a\webright ]\webright )\webright ]\webleft (\star ,\star \webright )\\ & = \webleft [\sigma ^{\prime ,-1}_{A,B}\circ \text{id}^{\otimes ,-1}_{\mathsf{Sets}|B,A}\circ \webleft (\webleft [b\webright ]\times \webleft [a\webright ]\webright )\webright ]\webleft (\star ,\star \webright )\\ & = \webleft [\sigma ^{\prime ,-1}_{A,B}\circ \text{id}^{\otimes ,-1}_{\mathsf{Sets}|B,A}\webright ]\webleft (b,a\webright ) \end{align*}

for each $\webleft (b,a\webright )\in B\times A$, and thus we have

\[ \text{id}^{\otimes ,-1}_{\mathsf{Sets}|A,B}\circ \sigma ^{\mathsf{Sets},-1}_{A,B}=\sigma ^{\prime ,-1}_{A,B}\circ \text{id}^{\otimes ,-1}_{\mathsf{Sets}|B,A}. \]

Taking inverses then gives

\[ \sigma ^{\mathsf{Sets}}_{A,B}\circ \text{id}^{\otimes }_{\mathsf{Sets}|A,B}=\text{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 _{\text{pt},B},\\ \lambda '_{B} & = \lambda ^{\mathsf{Sets}}_{B}\circ \psi _{\text{pt},B}. \end{align*}

Postcomposing both sides by $\lambda ^{\mathsf{Sets},-1}_{B}$ gives

\begin{align*} \lambda ^{\mathsf{Sets},-1}_{B}\circ \lambda '_{B} & = \phi _{\text{pt},B},\\ \lambda ^{\mathsf{Sets},-1}_{B}\circ \lambda '_{B} & = \psi _{\text{pt},B}, \end{align*}

and thus we have

\[ \phi _{\text{pt},B}=\psi _{\text{pt},B} \]

for each $B\in \text{Obj}\webleft (\mathsf{Sets}\webright )$. Now, let $a\in A$ and consider the naturality diagrams

for $\phi $ and $\psi $ with respect to the morphisms $\webleft [a\webright ]$ and $\text{id}_{B}$. Having shown that $\phi _{\text{pt},B}=\psi _{\text{pt},B}$, we have

\begin{align*} \phi _{A,B}\webleft (a,b\webright ) & = \webleft [\phi _{A,B}\circ \webleft (\webleft [a\webright ]\times \text{id}_{B}\webright )\webright ]\webleft (\star ,b\webright )\\ & = \webleft [\webleft (\webleft [a\webright ]\otimes _{\mathsf{Sets}}\text{id}_{B}\webright )\circ \phi _{\text{pt},B}\webright ]\webleft (\star ,b\webright )\\ & = \webleft [\webleft (\webleft [a\webright ]\otimes _{\mathsf{Sets}}\text{id}_{B}\webright )\circ \psi _{\text{pt},B}\webright ]\webleft (\star ,b\webright )\\ & = \webleft [\psi _{A,B}\circ \webleft (\webleft [a\webright ]\times \text{id}_{B}\webright )\webright ]\webleft (\star ,b\webright )\\ & = \psi _{A,B}\webleft (a,b\webright ) \end{align*}

for each $\webleft (a,b\webright )\in A\times B$. Therefore we have

\[ \phi _{A,B}=\psi _{A,B} \]

for each $A,B\in \text{Obj}\webleft (\mathsf{Sets}\webright )$ and thus $\phi =\psi $, showing the isomorphism $\mathord {\otimes _{\mathsf{Sets}}}\cong \mathord {\times }$ to be unique.


Noticed something off, or have any comments? Feel free to reach out!


You can also use the contact form below: