The product of $A$ and $B$1 is the product of $A$ and $B$ in $\mathsf{Sets}$ as in 
, .
- 1Further Terminology: Also called the Cartesian product of $A$ and $B$.
-
1.
The Limit. The set $A\times B$ defined by
\begin{align*} A\times B & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\prod _{z\in \left\{ A,B\right\} }z\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ f\in \mathsf{Sets}(\left\{ 0,1\right\} ,A\cup B)\ \middle |\ \text{we have $f(0)\in A$ and $f(1)\in B$}\right\} \\ & \cong \left\{ \left\{ \left\{ a\right\} ,\left\{ a,b\right\} \right\} \in \mathcal{P}(\mathcal{P}(A\cup B))\ \middle |\ \text{we have $a\in A$ and $b\in B$}\right\} \\ & \cong \left\{ \begin{aligned} & \text{ordered pairs $(a,b)$ with}\\ & \text{$a\in A$ and $b\in B$}\end{aligned} \right\} .\end{align*} -
2.
The Cone. The maps
\begin{align*} \operatorname {\mathrm{\mathrm{pr}}}_{1} & \colon A\times B\to A,\\ \operatorname {\mathrm{\mathrm{pr}}}_{2} & \colon A\times B\to B \end{align*}defined by
\begin{align*} \operatorname {\mathrm{\mathrm{pr}}}_{1}(a,b) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}a,\\ \operatorname {\mathrm{\mathrm{pr}}}_{2}(a,b) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}b \end{align*}for each $(a,b)\in A\times B$.
-
1.
Functoriality. The assignments $A,B,(A,B)\mapsto A\times B$ define functors
\[ \begin{array}{ccc} A\times -\colon \mkern -15mu & \mathsf{Sets} \mkern -17.5mu& {}\mathbin {\to }\mathsf{Sets},\\ -\times B\colon \mkern -15mu & \mathsf{Sets} \mkern -17.5mu& {}\mathbin {\to }\mathsf{Sets},\\ -_{1}\times -_{2}\colon \mkern -15mu & \mathsf{Sets}\times \mathsf{Sets} \mkern -17.5mu& {}\mathbin {\to }\mathsf{Sets}, \end{array} \]where $-_{1}\times -_{2}$ is the functor where
-
•
Action on Objects. For each $(A,B)\in \operatorname {\mathrm{Obj}}(\mathsf{Sets}\times \mathsf{Sets})$, we have
\[ [-_{1}\times -_{2}](A,B)\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}A\times B. \] -
•
Action on Morphisms. For each $(A,B),(X,Y)\in \operatorname {\mathrm{Obj}}(\mathsf{Sets})$, the action on $\operatorname {\mathrm{Hom}}$-sets
\[ \mathord {\times }_{(A,B),(X,Y)} \colon \mathsf{Sets}(A,X)\times \mathsf{Sets}(B,Y)\to \mathsf{Sets}(A\times B,X\times Y) \]of $\times $ at $((A,B),(X,Y))$ is defined by sending $(f,g)$ to the function
\[ f\times g\colon A\times B\to X\times Y \]defined by
\[ [f\times g](a,b)\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}(f(a),g(b)) \]for each $(a,b)\in A\times B$.
and where $A\times -$ and $-\times B$ are the partial functors of $-_{1}\times -_{2}$ at $A,B\in \operatorname {\mathrm{Obj}}(\mathsf{Sets})$.
-
•
-
2.
Adjointness I. We have adjunctions
witnessed by bijections
\begin{align*} \mathsf{Sets}(A\times B,C) & \cong \mathsf{Sets}(A,\mathsf{Sets}(B,C)),\\ \mathsf{Sets}(A\times B,C) & \cong \mathsf{Sets}(B,\mathsf{Sets}(A,C)), \end{align*}natural in $A,B,C\in \operatorname {\mathrm{Obj}}(\mathsf{Sets})$.
-
3.
Adjointness II. We have an adjunction
witnessed by a bijection
\[ \operatorname {\mathrm{Hom}}_{\mathsf{Sets}\times \mathsf{Sets}}((A,A),(B,C))\cong \mathsf{Sets}(A,B\times C), \]natural in $A\in \operatorname {\mathrm{Obj}}(\mathsf{Sets})$ and in $(B,C)\in \operatorname {\mathrm{Obj}}(\mathsf{Sets}\times \mathsf{Sets})$.
-
4.
Associativity. We have an isomorphism of sets
\[ \alpha ^{\mathsf{Sets}}_{A,B,C}\colon (A\times B)\times C\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }A\times (B\times C), \]natural in $A,B,C\in \operatorname {\mathrm{Obj}}(\mathsf{Sets})$.
-
5.
Unitality. We have isomorphisms of sets
\begin{align*} \lambda ^{\mathsf{Sets}}_{A} & \colon \mathrm{pt}\times A \overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }A,\\ \rho ^{\mathsf{Sets}}_{A} & \colon A\times \mathrm{pt}\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }A, \end{align*}natural in $A\in \operatorname {\mathrm{Obj}}(\mathsf{Sets})$.
-
6.
Commutativity. We have an isomorphism of sets
\[ \sigma ^{\mathsf{Sets}}_{A,B}\colon A\times B \overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }B\times A, \]natural in $A,B\in \operatorname {\mathrm{Obj}}(\mathsf{Sets})$.
-
7.
Distributivity Over Coproducts. We have isomorphisms of sets
\begin{align*} \delta ^{\mathsf{Sets}}_{\ell } & \colon A\times (B\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}C) \overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }(A\times B)\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}(A\times C),\\ \delta ^{\mathsf{Sets}}_{r} & \colon (A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}B)\times C \overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }(A\times C)\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}(B\times C), \end{align*}natural in $A,B,C\in \operatorname {\mathrm{Obj}}(\mathsf{Sets})$.
-
8.
Annihilation With the Empty Set. We have isomorphisms of sets
\begin{align*} \zeta ^{\mathsf{Sets}}_{\ell } & \colon \text{Ø}\times A \overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }\text{Ø},\\ \zeta ^{\mathsf{Sets}}_{r} & \colon A\times \text{Ø}\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }\text{Ø}, \end{align*}natural in $A\in \operatorname {\mathrm{Obj}}(\mathsf{Sets})$.
-
9.
Distributivity Over Unions. Let $X$ be a set. For each $U,V,W\in \mathcal{P}(X)$, we have equalities
\begin{align*} U\times (V\cup W) & = (U\times V)\cup (U\times W),\\ (U\cup V)\times W & = (U\times W)\cup (V\times W) \end{align*}of subsets of $\mathcal{P}(X\times X)$.
-
10.
Distributivity Over Intersections. Let $X$ be a set. For each $U,V,W\in \mathcal{P}(X)$, we have equalities
\begin{align*} U\times (V\cap W) & = (U\times V)\cap (U\times W),\\ (U\cap V)\times W & = (U\times W)\cap (V\times W) \end{align*}of subsets of $\mathcal{P}(X\times X)$.
-
11.
Distributivity Over Differences. Let $X$ be a set. For each $U,V,W\in \mathcal{P}(X)$, we have equalities
\begin{align*} U\times (V\setminus W) & = (U\times V)\setminus (U\times W),\\ (U\setminus V)\times W & = (U\times W)\setminus (V\times W) \end{align*}of subsets of $\mathcal{P}(X\times X)$.
-
12.
Distributivity Over Symmetric Differences. Let $X$ be a set. For each $U,V,W\in \mathcal{P}(X)$, we have equalities
\begin{align*} U\times (V\mathbin {\triangle }W) & = (U\times V)\mathbin {\triangle }(U\times W),\\ (U\mathbin {\triangle }V)\times W & = (U\times W)\mathbin {\triangle }(V\times W) \end{align*}of subsets of $\mathcal{P}(X\times X)$.
-
13.
Middle-Four Exchange with Respect to Intersections. The diagram
commutes, i.e. we have
\[ (U\times V)\cap (W\times T)=(U\cap V)\times (W\cap T). \]for each $U,V,W,T\in \mathcal{P}(X)$.
-
14.
Symmetric Monoidality. The 8-tuple $\left(\phantom{\mathrlap {\alpha ^{\mathsf{Sets}}}}\mathsf{Sets}\right.$, $\times $, $\mathrm{pt}$, $\mathsf{Sets}(-_{1},-_{2})$, $\alpha ^{\mathsf{Sets}}$, $\lambda ^{\mathsf{Sets}}$, $\rho ^{\mathsf{Sets}}$, $\left.\sigma ^{\mathsf{Sets}}\right)$ is a closed symmetric monoidal category.
-
15.
Symmetric Bimonoidality. The 18-tuple
\[ \begin{aligned} & \left(\mathsf{Sets},\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }},\times ,\text{Ø},\mathrm{pt},\mathsf{Sets}(-_{1},-_{2}),\alpha ^{\mathsf{Sets}},\lambda ^{\mathsf{Sets}},\rho ^{\mathsf{Sets}},\sigma ^{\mathsf{Sets}},\right.\\ & \left.\alpha ^{\mathsf{Sets},\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}},\lambda ^{\mathsf{Sets},\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}},\rho ^{\mathsf{Sets},\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}},\sigma ^{\mathsf{Sets},\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}},\delta ^{\mathsf{Sets}}_{\ell },\delta ^{\mathsf{Sets}}_{r},\zeta ^{\mathsf{Sets}}_{\ell },\zeta ^{\mathsf{Sets}}_{r}\right),\end{aligned} \]is a symmetric closed bimonoidal category, where $\alpha ^{\mathsf{Sets},\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}$, $\lambda ^{\mathsf{Sets},\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}$, $\rho ^{\mathsf{Sets},\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}$, and $\sigma ^{\mathsf{Sets},\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}$ are the natural transformations from Item 3, Item 4, and Item 5 of Proposition 4.2.3.1.3.
-
•
Map I. We define a map
\[ \Phi _{B,C}\colon \mathsf{Sets}(A\times B,C)\to \mathsf{Sets}(A,\mathsf{Sets}(B,C)), \]by sending a function
\[ \xi \colon A\times B\to C \]to the function
where we define
\[ \xi ^{\dagger }_{a}(b)\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi (a,b) \]for each $b\in B$. In terms of the $[\mspace {-3mu}[a\mapsto f(a)]\mspace {-3mu}]$ notation of Chapter 3: Sets, Notation 3.1.1.1.2, we have
\[ \xi ^{\dagger }\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}[\mspace {-3mu}[a\mapsto [\mspace {-3mu}[b\mapsto \xi (a,b)]\mspace {-3mu}]]\mspace {-3mu}]. \] -
•
Map II. We define a map
\[ \Psi _{B,C}\colon \mathsf{Sets}(A,\mathsf{Sets}(B,C)),\to \mathsf{Sets}(A\times B,C) \]given by sending a function
to the function
\[ \xi ^{\dagger }\colon A\times B\to C \]defined by
\begin{align*} \xi ^{\dagger }(a,b) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\mathrm{ev}_{b}(\mathrm{ev}_{a}(\xi ))\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\mathrm{ev}_{b}(\xi _{a})\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi _{a}(b)\end{align*}for each $(a,b)\in A\times B$.
-
•
Invertibility I. We claim that
\[ \Psi _{A,B}\circ \Phi _{A,B}=\operatorname {\mathrm{id}}_{\mathsf{Sets}(A\times B,C)}. \]Indeed, given a function $\xi \colon A\times B\to C$, we have
\begin{align*} [\Psi _{A,B}\circ \Phi _{A,B}](\xi ) & = \Psi _{A,B}(\Phi _{A,B}(\xi ))\\ & = \Psi _{A,B}(\Phi _{A,B}([\mspace {-3mu}[(a,b)\mapsto \xi (a,b)]\mspace {-3mu}]))\\ & = \Psi _{A,B}([\mspace {-3mu}[a\mapsto [\mspace {-3mu}[b\mapsto \xi (a,b)]\mspace {-3mu}]]\mspace {-3mu}])\\ & = \Psi _{A,B}([\mspace {-3mu}[a'\mapsto [\mspace {-3mu}[b'\mapsto \xi (a',b')]\mspace {-3mu}]]\mspace {-3mu}])\\ & = [\mspace {-3mu}[(a,b)\mapsto \mathrm{ev}_{b}(\mathrm{ev}_{a}([\mspace {-3mu}[a'\mapsto [\mspace {-3mu}[b'\mapsto \xi (a',b')]\mspace {-3mu}]]\mspace {-3mu}]))]\mspace {-3mu}]\\ & = [\mspace {-3mu}[(a,b)\mapsto \mathrm{ev}_{b}([\mspace {-3mu}[b'\mapsto \xi (a,b')]\mspace {-3mu}])]\mspace {-3mu}]\\ & = [\mspace {-3mu}[(a,b)\mapsto \xi (a,b)]\mspace {-3mu}]\\ & = \xi . \end{align*} -
•
Invertibility II. We claim that
\[ \Phi _{A,B}\circ \Psi _{A,B}=\operatorname {\mathrm{id}}_{\mathsf{Sets}(A,\mathsf{Sets}(B,C))}. \]Indeed, given a function
we have
\begin{align*} [\Phi _{A,B}\circ \Psi _{A,B}](\xi ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\Phi _{A,B}(\Psi _{A,B}(\xi ))\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\Phi _{A,B}([\mspace {-3mu}[(a,b)\mapsto \xi _{a}(b)]\mspace {-3mu}])\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\Phi _{A,B}([\mspace {-3mu}[(a',b')\mapsto \xi _{a'}(b')]\mspace {-3mu}])\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}[\mspace {-3mu}[a\mapsto [\mspace {-3mu}[b\mapsto \mathrm{ev}_{(a,b)}([\mspace {-3mu}[(a',b')\mapsto \xi _{a'}(b')]\mspace {-3mu}])]\mspace {-3mu}]]\mspace {-3mu}]\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}[\mspace {-3mu}[a\mapsto [\mspace {-3mu}[b\mapsto \xi _{a}(b)]\mspace {-3mu}]]\mspace {-3mu}]\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}[\mspace {-3mu}[a\mapsto \xi _{a}]\mspace {-3mu}]\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi .\end{align*} -
•
Naturality for $\Phi $, Part I. We need to show that, given a function $g\colon B\to B'$, the diagram
commutes. Indeed, given a function
\[ \xi \colon A\times B'\to C, \]we have
\begin{align*} [\Phi _{B,C}\circ (\operatorname {\mathrm{id}}_{A}\times g^{*})](\xi ) & = \Phi _{B,C}([\operatorname {\mathrm{id}}_{A}\times g^{*}](\xi ))\\ & = \Phi _{B,C}(\xi (-_{1},g(-_{2})))\\ & = [\xi (-_{1},g(-_{2}))]^{\dagger }\\ & = \xi ^{\dagger }_{-_{1}}(g(-_{2}))\\ & = (g^{*})_{!}(\xi ^{\dagger })\\ & = (g^{*})_{!}(\Phi _{B',C}(\xi ))\\ & = [(g^{*})_{!}\circ \Phi _{B',C}](\xi ). \end{align*}Alternatively, using the $[\mspace {-3mu}[a\mapsto f(a)]\mspace {-3mu}]$ notation of Chapter 3: Sets, Notation 3.1.1.1.2, we have
\begin{align*} [\Phi _{B,C}\circ (\operatorname {\mathrm{id}}_{A}\times g^{*})](\xi ) & = \Phi _{B,C}([\operatorname {\mathrm{id}}_{A}\times g^{*}](\xi ))\\ & = \Phi _{B,C}([\operatorname {\mathrm{id}}_{A}\times g^{*}]([\mspace {-3mu}[(a,b')\mapsto \xi (a,b')]\mspace {-3mu}]))\\ & = \Phi _{B,C}([\mspace {-3mu}[(a,b)\mapsto \xi (a,g(b))]\mspace {-3mu}])\\ & = [\mspace {-3mu}[a\mapsto [\mspace {-3mu}[b\mapsto \xi (a,g(b))]\mspace {-3mu}]]\mspace {-3mu}]\\ & = [\mspace {-3mu}[a\mapsto g^{*}([\mspace {-3mu}[b'\mapsto \xi (a,b')]\mspace {-3mu}])]\mspace {-3mu}]\\ & = (g^{*})_{!}([\mspace {-3mu}[a\mapsto [\mspace {-3mu}[b'\mapsto \xi (a,b')]\mspace {-3mu}]]\mspace {-3mu}])\\ & = (g^{*})_{!}(\Phi _{B',C}([\mspace {-3mu}[(a,b')\mapsto \xi (a,b')]\mspace {-3mu}]))\\ & = (g^{*})_{!}(\Phi _{B',C}(\xi ))\\ & = [(g^{*})_{!}\circ \Phi _{B',C}](\xi ). \end{align*} -
•
Naturality for $\Phi $, Part II. We need to show that, given a function $h\colon C\to C'$, the diagram
commutes. Indeed, given a function
\[ \xi \colon A\times B\to C, \]we have
\begin{align*} [\Phi _{B,C}\circ h_{!}](\xi ) & = \Phi _{B,C}(h_{!}(\xi ))\\ & = \Phi _{B,C}(h_{!}([\mspace {-3mu}[(a,b)\mapsto \xi (a,b)]\mspace {-3mu}]))\\ & = \Phi _{B,C}([\mspace {-3mu}[(a,b)\mapsto h(\xi (a,b))]\mspace {-3mu}])\\ & = [\mspace {-3mu}[a\mapsto [\mspace {-3mu}[b\mapsto h(\xi (a,b))]\mspace {-3mu}]]\mspace {-3mu}]\\ & = [\mspace {-3mu}[a\mapsto h_{!}([\mspace {-3mu}[b\mapsto \xi (a,b)]\mspace {-3mu}]]\mspace {-3mu}])\\ & = (h_{!})_{!}([\mspace {-3mu}[a\mapsto [\mspace {-3mu}[b\mapsto \xi (a,b)]\mspace {-3mu}]]\mspace {-3mu}])\\ & = (h_{!})_{!}(\Phi _{B,C}([\mspace {-3mu}[(a,b)\mapsto \xi (a,b)]\mspace {-3mu}]))\\ & = (h_{!})_{!}(\Phi _{B,C}(\xi ))\\ & = [(h_{!})_{!}\circ \Phi _{B,C}](\xi ). \end{align*} -
•
Naturality for $\Psi $. Since $\Phi $ is natural in each argument and $\Phi $ is a componentwise inverse to $\Psi $ in each argument, it follows from Chapter 11: Categories, Item 2 of Proposition 11.9.7.1.2 that $\Psi $ is also natural in each argument.
4.1.3 Binary Products of Sets
Let $A$ and $B$ be sets.
Concretely, the product of $A$ and $B$ is the pair $\smash {(A\times B,\left\{ \operatorname {\mathrm{\mathrm{pr}}}_{1},\operatorname {\mathrm{\mathrm{pr}}}_{2}\right\} )}$ consisting of:
Proof of Construction 4.1.3.1.2.
We claim that $A\times B$ is the categorical product of $A$ and $B$ in the category of sets. Indeed, suppose we have a diagram of the form
\begin{align*} \operatorname {\mathrm{\mathrm{pr}}}_{1}\circ \phi & = p_{1},\\ \operatorname {\mathrm{\mathrm{pr}}}_{2}\circ \phi & = p_{2} \end{align*}
via
\[ \phi (x)=(p_{1}(x),p_{2}(x)) \]
for each $x\in P$.
Let $A$, $B$, $C$, and $X$ be sets.
Proof of Proposition 4.1.3.1.3.
Item 1: Functoriality
This follows from , of .
Item 2: Adjointness
We prove only that there’s an adjunction $-\times B\dashv \mathsf{Sets}(B,-)$, witnessed by a bijection
\[ \mathsf{Sets}(A\times B,C)\cong \mathsf{Sets}(A,\mathsf{Sets}(B,C)), \]
natural in $B,C\in \operatorname {\mathrm{Obj}}(\mathsf{Sets})$, as the proof of the existence of the adjunction $A\times -\dashv \mathsf{Sets}(A,-)$ follows almost exactly in the same way.
This finishes the proof.
Item 3: Adjointness II
This follows from the universal property of the product.
Item 4: Associativity
This is proved in the proof of Chapter 5: Monoidal Structures on the Category of Sets, Definition 5.1.4.1.1.
Item 5: Unitality
This is proved in the proof of Chapter 5: Monoidal Structures on the Category of Sets, Definition 5.1.5.1.1 and Definition 5.1.6.1.1.
Item 6: Commutativity
This is proved in the proof of Chapter 5: Monoidal Structures on the Category of Sets, Definition 5.1.7.1.1.
Item 7: Distributivity Over Coproducts
This is proved in the proof of Chapter 5: Monoidal Structures on the Category of Sets, Definition 5.3.1.1.1 and Definition 5.3.2.1.1.
Item 8: Annihilation With the Empty Set
This is proved in the proof of Chapter 5: Monoidal Structures on the Category of Sets, Definition 5.3.3.1.1 and Definition 5.3.4.1.1.
Item 9: Distributivity Over Unions
See [Proof Wiki Contributors, Cartesian Product Distributes Over Union — Proof Wiki].
Item 10: Distributivity Over Intersections
See Corollary 1 of [Proof Wiki Contributors, Cartesian Product of Intersections — Proof Wiki].
Item 11: Distributivity Over Differences
See [Proof Wiki Contributors, Cartesian Product Distributes Over Set Difference — Proof Wiki].
Item 12: Distributivity Over Symmetric Differences
See [Proof Wiki Contributors, Cartesian Product Distributes Over Symmetric Difference — Proof Wiki].
Item 13: Middle-Four Exchange With Respect to Intersections
See Corollary 1 of [Proof Wiki Contributors, Cartesian Product of Intersections — Proof Wiki].
Item 14: Symmetric Monoidality
This is a repetition of Chapter 5: Monoidal Structures on the Category of Sets, Proposition 5.1.9.1.1, and is proved there.
Item 15: Symmetric Bimonoidality
This is a repetition of Chapter 5: Monoidal Structures on the Category of Sets, Proposition 5.3.5.1.1, and is proved there.
As shown in Item 1 of Proposition 4.1.3.1.3, the Cartesian product of sets defines a functor
\[ -_{1}\times -_{2}\colon \mathsf{Sets}\times \mathsf{Sets}\to \mathsf{Sets}. \]
This functor is the $(k,\ell )=(-1,-1)$ case of a family of functors
\[ \otimes _{k,\ell }\colon \mathsf{Mon}_{\mathbb {E}_{k}}(\mathsf{Sets})\times \mathsf{Mon}_{\mathbb {E}_{\ell }}(\mathsf{Sets})\to \mathsf{Mon}_{\mathbb {E}_{k+\ell }}(\mathsf{Sets}) \]
of tensor products of $\mathbb {E}_{k}$-monoid objects on $\mathsf{Sets}$ with $\mathbb {E}_{\ell }$-monoid objects on $\mathsf{Sets}$; see .
We may state the equalities in Item 9, Item 10, Item 11, and Item 12 of Proposition 4.1.3.1.3 as the commutativity of the following diagrams:
