The Clowder Project

Let $X$ be a set.

1. Co/Completeness. The (posetal) category (associated to) $\webleft (\mathcal{P}\webleft (X\webright ),\subset \webright )$ is complete and cocomplete:
   1. Products. The products in $\mathcal{P}\webleft (X\webright )$ are given by intersection of subsets.
   2. Coproducts. The coproducts in $\mathcal{P}\webleft (X\webright )$ are given by union of subsets.
   3. Co/Equalisers. Being a posetal category, $\mathcal{P}\webleft (X\webright )$ only has at most one morphisms between any two objects, so co/equalisers are trivial.
2. Cartesian Closedness. The category $\mathcal{P}\webleft (X\webright )$ is Cartesian closed.
3. Powersets as Sets of Relations. We have bijections
   \begin{align*} \mathcal{P}\webleft (X\webright ) & \cong \mathrm{Rel}\webleft (\text{pt},X\webright ),\\ \mathcal{P}\webleft (X\webright ) & \cong \mathrm{Rel}\webleft (X,\text{pt}\webright ), \end{align*}

   natural in $X\in \text{Obj}\webleft (\mathsf{Sets}\webright )$.

4. Interaction With Products I. The map
   
   is an isomorphism of sets, natural in $X,Y\in \text{Obj}\webleft (\mathsf{Sets}\webright )$ with respect to each of the functor structures $\mathcal{P}_{*}$, $\mathcal{P}^{-1}$, and $\mathcal{P}_{!}$ on $\mathcal{P}$ of Proposition 2.4.2.1.1. Moreover, this makes $\mathcal{P}_{*}$, $\mathcal{P}^{-1}$, and $\mathcal{P}_{!}$ into symmetric monoidal functors.
5. Interaction With Products II. The map
   
   where
   \[ U\boxtimes _{X\times Y}V\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ \webleft (u,v\webright )\in X\times Y\ \middle |\ \text{$u\in U$ and $v\in V$}\webright\} \]

   is an inclusion of sets, natural in $X,Y\in \text{Obj}\webleft (\mathsf{Sets}\webright )$ with respect to each of the functor structures $\mathcal{P}_{*}$, $\mathcal{P}^{-1}$, and $\mathcal{P}_{!}$ on $\mathcal{P}$ of Proposition 2.4.2.1.1. Moreover, this makes $\mathcal{P}_{*}$, $\mathcal{P}^{-1}$, and $\mathcal{P}_{!}$ into symmetric monoidal functors.

6. Interaction With Products III. We have an isomorphism
   \[ \mathcal{P}\webleft (X\webright )\otimes \mathcal{P}\webleft (Y\webright )\cong \mathcal{P}\webleft (X\times Y\webright ), \]

   natural in $X,Y\in \text{Obj}\webleft (\mathsf{Sets}\webright )$ with respect to each of the functor structures $\mathcal{P}_{*}$, $\mathcal{P}^{-1}$, and $\mathcal{P}_{!}$ on $\mathcal{P}$ of Proposition 2.4.2.1.1, where $\otimes $ denotes the tensor product of suplattices of . Moreover, this makes $\mathcal{P}_{*}$, $\mathcal{P}^{-1}$, and $\mathcal{P}_{!}$ into symmetric monoidal functors.