Let
- 1.
Functoriality. The assignments
define functorswhere
is the functor where- Action on Objects. For each
, we have - Action on Morphisms. For each
, the action on -setsof
at is defined by sending to the functiondefined by
for each
.
and are the partial functors of at . - Action on Objects. For each
- 2.
Adjointness. We have adjunctions witnessed by bijections
natural in
. - 3.
Associativity. We have an isomorphism of sets
natural in
. - 4.
Unitality. We have isomorphisms of sets
natural in
. - 5.
Commutativity. We have an isomorphism of sets
natural in
. - 6.
Distributivity Over Coproducts. We have isomorphisms of sets
natural in
. - 7.
Annihilation With the Empty Set. We have isomorphisms of sets
natural in
. - 8.
Distributivity Over Unions. Let
be a set. For each , we have equalitiesof subsets of
. - 9.
Distributivity Over Intersections. Let
be a set. For each , we have equalitiesof subsets of
. - 10.
Distributivity Over Differences. Let
be a set. For each , we have equalitiesof subsets of
. - 11.
Distributivity Over Symmetric Differences. Let
be a set. For each , we have equalitiesof subsets of
. - 12.
Middle-Four Exchange with Respect to Intersections. The diagram
commutes, i.e. we have
for each
. - 13.
Symmetric Monoidality. The 8-tuple
, , , , , , , is a closed symmetric monoidal category. - 14.
Symmetric Bimonoidality. The 18-tuple
is a symmetric closed bimonoidal category, where
, , , and are the natural transformations from Item 2, Item 3, and Item 4 of Proposition 2.2.3.1.3.