Let $A$, $B$, $C$, and $X$ be sets.
-
Functoriality. The assignments $A,B,\webleft (A,B\webright )\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 $\webleft (A,B\webright )\in \text{Obj}\webleft (\mathsf{Sets}\times \mathsf{Sets}\webright )$, we have
\[ \webleft [-_{1}\times -_{2}\webright ]\webleft (A,B\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}A\times B. \]
- Action on Morphisms. For each $\webleft (A,B\webright ),\webleft (X,Y\webright )\in \text{Obj}\webleft (\mathsf{Sets}\webright )$, the action on $\textup{Hom}$-sets
\[ \times _{\webleft (A,B\webright ),\webleft (X,Y\webright )} \colon \mathsf{Sets}\webleft (A,X\webright )\times \mathsf{Sets}\webleft (B,Y\webright )\to \mathsf{Sets}\webleft (A\times B,X\times Y\webright ) \]
of $\times $ at $\webleft (\webleft (A,B\webright ),\webleft (X,Y\webright )\webright )$ is defined by sending $\webleft (f,g\webright )$ to the function
\[ f\times g\colon A\times B\to X\times Y \]
defined by
\[ \webleft [f\times g\webright ]\webleft (a,b\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft (f\webleft (a\webright ),g\webleft (b\webright )\webright ) \]
for each $\webleft (a,b\webright )\in A\times B$.
and where $A\times -$ and $-\times B$ are the partial functors of $-_{1}\times -_{2}$ at $A,B\in \text{Obj}\webleft (\mathsf{Sets}\webright )$.
-
Adjointness. We have adjunctions witnessed by bijections
\begin{align*} \mathsf{Sets}\webleft (A\times B,C\webright ) & \cong \mathsf{Sets}\webleft (A,\mathsf{Sets}\webleft (B,C\webright )\webright ),\\ \mathsf{Sets}\webleft (A\times B,C\webright ) & \cong \mathsf{Sets}\webleft (B,\mathsf{Sets}\webleft (A,C\webright )\webright ), \end{align*}
natural in $A,B,C\in \text{Obj}\webleft (\mathsf{Sets}\webright )$.
-
Associativity. We have an isomorphism of sets
\[ \alpha ^{\mathsf{Sets}}_{A,B,C}\colon \webleft (A\times B\webright )\times C\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }A\times \webleft (B\times C\webright ), \]
natural in $A,B,C\in \text{Obj}\webleft (\mathsf{Sets}\webright )$.
-
Unitality. We have isomorphisms of sets
\begin{align*} \lambda ^{\mathsf{Sets}}_{A} & \colon \text{pt}\times A \overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }A,\\ \rho ^{\mathsf{Sets}}_{A} & \colon A\times \text{pt}\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }A, \end{align*}
natural in $A\in \text{Obj}\webleft (\mathsf{Sets}\webright )$.
-
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 \text{Obj}\webleft (\mathsf{Sets}\webright )$.
-
Distributivity Over Coproducts. We have isomorphisms of sets
\begin{align*} \delta ^{\mathsf{Sets}}_{\ell } & \colon A\times \webleft (B\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}C\webright ) \overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }\webleft (A\times B\webright )\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}\webleft (A\times C\webright ),\\ \delta ^{\mathsf{Sets}}_{r} & \colon \webleft (A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}B\webright )\times C \overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }\webleft (A\times C\webright )\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}\webleft (B\times C\webright ), \end{align*}
natural in $A,B,C\in \text{Obj}\webleft (\mathsf{Sets}\webright )$.
-
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 \text{Obj}\webleft (\mathsf{Sets}\webright )$.
-
Distributivity Over Unions. Let $X$ be a set. For each $U,V,W\in \mathcal{P}\webleft (X\webright )$, we have equalities
\begin{align*} U\times \webleft (V\cup W\webright ) & = \webleft (U\times V\webright )\cup \webleft (U\times W\webright ),\\ \webleft (U\cup V\webright )\times W & = \webleft (U\times W\webright )\cup \webleft (V\times W\webright ) \end{align*}
of subsets of $\mathcal{P}\webleft (X\times X\webright )$.
-
Distributivity Over Intersections. Let $X$ be a set. For each $U,V,W\in \mathcal{P}\webleft (X\webright )$, we have equalities
\begin{align*} U\times \webleft (V\cap W\webright ) & = \webleft (U\times V\webright )\cap \webleft (U\times W\webright ),\\ \webleft (U\cap V\webright )\times W & = \webleft (U\times W\webright )\cap \webleft (V\times W\webright ) \end{align*}
of subsets of $\mathcal{P}\webleft (X\times X\webright )$.
-
Distributivity Over Differences. Let $X$ be a set. For each $U,V,W\in \mathcal{P}\webleft (X\webright )$, we have equalities
\begin{align*} U\times \webleft (V\setminus W\webright ) & = \webleft (U\times V\webright )\setminus \webleft (U\times W\webright ),\\ \webleft (U\setminus V\webright )\times W & = \webleft (U\times W\webright )\setminus \webleft (V\times W\webright ) \end{align*}
of subsets of $\mathcal{P}\webleft (X\times X\webright )$.
-
Distributivity Over Symmetric Differences. Let $X$ be a set. For each $U,V,W\in \mathcal{P}\webleft (X\webright )$, we have equalities
\begin{align*} U\times \webleft (V\mathbin {\triangle }W\webright ) & = \webleft (U\times V\webright )\mathbin {\triangle }\webleft (U\times W\webright ),\\ \webleft (U\mathbin {\triangle }V\webright )\times W & = \webleft (U\times W\webright )\mathbin {\triangle }\webleft (V\times W\webright ) \end{align*}
of subsets of $\mathcal{P}\webleft (X\times X\webright )$.
-
Middle-Four Exchange with Respect to Intersections. The diagram
commutes, i.e. we have
\[ \webleft (U\times V\webright )\cap \webleft (W\times T\webright )=\webleft (U\cap V\webright )\times \webleft (W\cap T\webright ). \]
for each $U,V,W,T\in \mathcal{P}\webleft (X\webright )$.
-
Symmetric Monoidality. The 8-tuple $\webleft(\phantom{\mathrlap {\alpha ^{\mathsf{Sets}}}}\mathsf{Sets}\right.$, $\times $, $\text{pt}$, $\mathsf{Sets}\webleft (-_{1},-_{2}\webright )$, $\alpha ^{\mathsf{Sets}}$, $\lambda ^{\mathsf{Sets}}$, $\rho ^{\mathsf{Sets}}$, $\left.\sigma ^{\mathsf{Sets}}\webright)$ is a closed symmetric monoidal category.
-
Symmetric Bimonoidality. The 18-tuple
\[ \begin{aligned} & \webleft(\mathsf{Sets},\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }},\times ,\text{Ø},\text{pt},\mathsf{Sets}\webleft (-_{1},-_{2}\webright ),\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}\webright),\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 2, Item 3, and Item 4 of Proposition 2.2.3.1.3.