The Clowder Project

Let $A$, $B$, $C$, and $X$ be sets.

1. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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.