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

  1. 1. Functoriality. The assignments A,B,(A,B)A×B define functors
    A×:SetsSets,×B:SetsSets,1×2:Sets×SetsSets,

    where 1×2 is the functor where

    • Action on Objects. For each (A,B)Obj(Sets×Sets), we have

      [1×2](A,B)=defA×B.

    • Action on Morphisms. For each (A,B),(X,Y)Obj(Sets), the action on Hom-sets

      ×(A,B),(X,Y):Sets(A,X)×Sets(B,Y)Sets(A×B,X×Y)

      of × at ((A,B),(X,Y)) is defined by sending (f,g) to the function

      f×g:A×BX×Y

      defined by

      [f×g](a,b)=def(f(a),g(b))

      for each (a,b)A×B.

    and where A× and ×B are the partial functors of 1×2 at A,BObj(Sets).

  2. 2. Adjointness. We have adjunctions
    witnessed by bijections
    Sets(A×B,C)Sets(A,Sets(B,C)),Sets(A×B,C)Sets(B,Sets(A,C)),

    natural in A,B,CObj(Sets).

  3. 3. Associativity. We have an isomorphism of sets
    αA,B,CSets:(A×B)×CA×(B×C),

    natural in A,B,CObj(Sets).

  4. 4. Unitality. We have isomorphisms of sets
    λASets:pt×AA,ρASets:A×ptA,

    natural in AObj(Sets).

  5. 5. Commutativity. We have an isomorphism of sets
    σA,BSets:A×BB×A,

    natural in A,BObj(Sets).

  6. 6. Distributivity Over Coproducts. We have isomorphisms of sets
    δSets:A×(BC)(A×B)(A×C),δrSets:(AB)×C(A×C)(B×C),

    natural in A,B,CObj(Sets).

  7. 7. Annihilation With the Empty Set. We have isomorphisms of sets
    ζSets:Ø×AØ,ζrSets:A×ØØ,

    natural in AObj(Sets).

  8. 8. Distributivity Over Unions. Let X be a set. For each U,V,WP(X), we have equalities
    U×(VW)=(U×V)(U×W),(UV)×W=(U×W)(V×W)

    of subsets of P(X×X).

  9. 9. Distributivity Over Intersections. Let X be a set. For each U,V,WP(X), we have equalities
    U×(VW)=(U×V)(U×W),(UV)×W=(U×W)(V×W)

    of subsets of P(X×X).

  10. 10. Distributivity Over Differences. Let X be a set. For each U,V,WP(X), we have equalities
    U×(VW)=(U×V)(U×W),(UV)×W=(U×W)(V×W)

    of subsets of P(X×X).

  11. 11. Distributivity Over Symmetric Differences. Let X be a set. For each U,V,WP(X), we have equalities
    U×(VW)=(U×V)(U×W),(UV)×W=(U×W)(V×W)

    of subsets of P(X×X).

  12. 12. Middle-Four Exchange with Respect to Intersections. The diagram

    commutes, i.e. we have

    (U×V)(W×T)=(UV)×(WT).

    for each U,V,W,TP(X).

  13. 13. Symmetric Monoidality. The 8-tuple (αSetsSets, ×, pt, Sets(1,2), αSets, λSets, ρSets, σSets) is a closed symmetric monoidal category.
  14. 14. Symmetric Bimonoidality. The 18-tuple
    (Sets,,×,Ø,pt,Sets(1,2),αSets,λSets,ρSets,σSets,αSets,,λSets,,ρSets,,σSets,,δSets,δrSets,ζSets,ζrSets),

    is a symmetric closed bimonoidal category, where αSets,, λSets,, ρSets,, and σSets, are the natural transformations from Item 2, Item 3, and Item 4 of Proposition 2.2.3.1.3.

Item 1: Functoriality
This follows from , of .
Item 2: Adjointness
We prove only that there’s an adjunction ×BSets(B,), witnessed by a bijection

Sets(A×B,C)Sets(A,Sets(B,C)),

natural in B,CObj(Sets), as the proof of the existence of the adjunction A×Sets(A,) follows almost exactly in the same way.

  • Map I. We define a map

    ΦB,C:Sets(A×B,C)Sets(A,Sets(B,C)),

    by sending a function

    ξ:A×BC

    to the function

    where we define

    ξa(b)=defξ(a,b)

    for each bB. In terms of the [[af(a)]] notation of Chapter 1: Sets, Notation 1.1.1.1.2, we have

    ξ=def[[a[[bξ(a,b)]]]].

  • Map II. We define a map

    ΨB,C:Sets(A,Sets(B,C)),Sets(A×B,C)

    given by sending a function

    to the function

    ξ:A×BC

    defined by

    ξ(a,b)=defevb(eva(ξ))=defevb(ξa)=defξa(b)

    for each (a,b)A×B.

  • Invertibility I. We claim that

    ΨA,BΦA,B=idSets(A×B,C).

    Indeed, given a function ξ:A×BC, we have

    [ΨA,BΦA,B](ξ)=ΨA,B(ΦA,B(ξ))=ΨA,B(ΦA,B([[(a,b)ξ(a,b)]]))=ΨA,B([[a[[bξ(a,b)]]]])=ΨA,B([[a[[bξ(a,b)]]]])=[[(a,b)evb(eva([[a[[bξ(a,b)]]]]))]]=[[(a,b)evb([[bξ(a,b)]])]]=[[(a,b)ξ(a,b)]]=ξ.

  • Invertibility II. We claim that

    ΦA,BΨA,B=idSets(A,Sets(B,C)).

    Indeed, given a function

    we have

    [ΦA,BΨA,B](ξ)=defΦA,B(ΨA,B(ξ))=defΦA,B([[(a,b)ξa(b)]])=defΦA,B([[(a,b)ξa(b)]])=def[[a[[bev(a,b)([[(a,b)ξa(b)]])]]]]=def[[a[[bξa(b)]]]]=def[[aξa]]=defξ.

  • Naturality for Φ, Part I. We need to show that, given a function g:BB, the diagram

    commutes. Indeed, given a function

    ξ:A×BC,

    we have

    [ΦB,C(idA×g)](ξ)=ΦB,C([idA×g](ξ))=ΦB,C(ξ(1,g(2)))=[ξ(1,g(2))]=ξ1(g(2))=(g)(ξ)=(g)(ΦB,C(ξ))=[(g)ΦB,C](ξ).

    Alternatively, using the [[af(a)]] notation of Chapter 1: Sets, Notation 1.1.1.1.2, we have

    [ΦB,C(idA×g)](ξ)=ΦB,C([idA×g](ξ))=ΦB,C([idA×g]([[(a,b)ξ(a,b)]]))=ΦB,C([[(a,b)ξ(a,g(b))]])=[[a[[bξ(a,g(b))]]]]=[[ag([[bξ(a,b)]])]]=(g)([[a[[bξ(a,b)]]]])=(g)(ΦB,C([[(a,b)ξ(a,b)]]))=(g)(ΦB,C(ξ))=[(g)ΦB,C](ξ).

  • Naturality for Φ, Part II. We need to show that, given a function h:CC, the diagram

    commutes. Indeed, given a function

    ξ:A×BC,

    we have

    [ΦB,Ch](ξ)=ΦB,C(h(ξ))=ΦB,C(h([[(a,b)ξ(a,b)]]))=ΦB,C([[(a,b)h(ξ(a,b))]])=[[a[[bh(ξ(a,b))]]]]=[[ah([[bξ(a,b)]]]])=(h)([[a[[bξ(a,b)]]]])=(h)(ΦB,C([[(a,b)ξ(a,b)]]))=(h)(ΦB,C(ξ))=[(h)ΦB,C](ξ).

  • Naturality for Ψ. Since Φ is natural in each argument and Φ is a componentwise inverse to Ψ in each argument, it follows from Chapter 9: Preorders, Item 2 of Proposition 9.9.7.1.2 that Ψ is also natural in each argument.
Item 3: Associativity
This is proved in the proof of Chapter 3: Monoidal Structures on the Category of Sets, Definition 3.1.4.1.1.
Item 4: Unitality
This is proved in the proof of Chapter 3: Monoidal Structures on the Category of Sets, Definition 3.1.5.1.1 and Definition 3.1.6.1.1.
Item 5: Commutativity
This is proved in the proof of Chapter 3: Monoidal Structures on the Category of Sets, Definition 3.1.7.1.1.
Item 6: Distributivity Over Coproducts
This is proved in the proof of Chapter 3: Monoidal Structures on the Category of Sets, Definition 3.3.1.1.1 and Definition 3.3.2.1.1.
Item 7: Annihilation With the Empty Set
This is proved in the proof of Chapter 3: Monoidal Structures on the Category of Sets, Definition 3.3.3.1.1 and Definition 3.3.4.1.1.
Item 8: Distributivity Over Unions
See [Proof Wiki, Cartesian Product Distributes Over Union].
Item 9: Distributivity Over Intersections
See Corollary 1 of [Proof Wiki, Cartesian Product of Intersections].
Item 10: Distributivity Over Differences
See [Proof Wiki, Cartesian Product Distributes Over Set Difference].
Item 11: Distributivity Over Symmetric Differences
See [Proof Wiki, Cartesian Product Distributes Over Symmetric Difference].
Item 12: Middle-Four Exchange With Respect to Intersections
See Corollary 1 of [Proof Wiki, Cartesian Product of Intersections].
Item 13: Symmetric Monoidality
This is a repetition of Chapter 3: Monoidal Structures on the Category of Sets, Proposition 3.1.9.1.1, and is proved there.
Item 14: Symmetric Bimonoidality
This is a repetition of Chapter 3: Monoidal Structures on the Category of Sets, Proposition 3.3.5.1.1, and is proved there.


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


You can also use the contact form below: