Let $A$ and $B$ be sets.
We claim that Item 1, Item 2, Item 3, Item 4, and Item 5 are indeed equivalent:
- Item 1$\iff $Item 2: This is a special case of Chapter 2: Constructions With Sets,
and of . - Item 2$\iff $Item 3: This follows from the bijections
\begin{align*} \mathsf{Sets}\webleft (A\times B,\{ \mathsf{true},\mathsf{false}\} \webright ) & \cong \mathsf{Sets}\webleft (A,\mathsf{Sets}\webleft (B,\{ \mathsf{true},\mathsf{false}\} \webright )\webright )\\ & \cong \mathsf{Sets}\webleft (A,\mathcal{P}\webleft (B\webright )\webright ), \end{align*}
where the last bijection is from Chapter 2: Constructions With Sets, and of .
- Item 2$\iff $Item 4: This follows from the bijections
\begin{align*} \mathsf{Sets}\webleft (A\times B,\{ \mathsf{true},\mathsf{false}\} \webright ) & \cong \mathsf{Sets}\webleft (B,\mathsf{Sets}\webleft (B,\{ \mathsf{true},\mathsf{false}\} \webright )\webright )\\ & \cong \mathsf{Sets}\webleft (B,\mathcal{P}\webleft (A\webright )\webright ), \end{align*}
where again the last bijection is from Chapter 2: Constructions With Sets, and of .
- Item 2$\iff $Item 5: This follows from the universal property of the powerset $\mathcal{P}\webleft (X\webright )$ of a set $X$ as the free cocompletion of $X$ via the characteristic embedding
\[ \chi _{X} \colon X \hookrightarrow \mathcal{P}\webleft (X\webright ) \]
of $X$ into $\mathcal{P}\webleft (X\webright )$, Chapter 2: Constructions With Sets, of .
In particular, the bijection
\[ \mathsf{Sets}\webleft (A,\mathcal{P}\webleft (B\webright )\webright )\cong \textup{Hom}^{\mathrm{cocont}}_{\mathsf{Pos}}\webleft (\mathcal{P}\webleft (A\webright ),\mathcal{P}\webleft (B\webright )\webright ) \]
is given by extending each $f\colon A\to \mathcal{P}\webleft (B\webright )$ in $\mathsf{Sets}\webleft (A,\mathcal{P}\webleft (B\webright )\webright )$ to all of $\mathcal{P}\webleft (A\webright )$ by taking its left Kan extension along $\chi _{X}$.
1
This coincides with the direct image function $f_{*}\colon \mathcal{P}\webleft (A\webright )\to \mathcal{P}\webleft (B\webright )$ of Chapter 2: Constructions With Sets, Definition 2.6.1.1.1.
This finishes the proof.
Item 1: End Formula for the Set of Inclusions of Relations
Unwinding the expression inside the end on the right hand side, we have
\[ \int _{a\in A}\int _{b\in B}\textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (R^{b}_{a},S^{b}_{a}\webright )\cong \begin{cases} \text{pt}& \text{if, for each $a\in A$ and each $b\in B$,}\\ & \text{we have $\textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (R^{b}_{a},S^{b}_{a}\webright )\cong \text{pt}$}\\ \text{Ø}& \text{otherwise.}\end{cases} \]
Since we have $\textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (R^{b}_{a},S^{b}_{a}\webright )=\webleft\{ \mathsf{true}\webright\} \cong \text{pt}$ exactly when $R^{b}_{a}=\mathsf{false}$ or $R^{b}_{a}=S^{b}_{a}=\mathsf{true}$, we get
\[ \int _{a\in A}\int _{b\in B}\textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (R^{b}_{a},S^{b}_{a}\webright )\cong \begin{cases} \text{pt}& \text{if, for each $a\in A$ and each $b\in B$,}\\ & \text{if $a\sim _{R}b$, then $a\sim _{S}b$,}\\ \text{Ø}& \text{otherwise.}\end{cases} \]
On the left hand-side, we have
\[ \textup{Hom}_{\mathbf{Rel}\webleft (A,B\webright )}\webleft (R,S\webright )\cong \begin{cases} \text{pt}& \text{if $R\subset S$,}\\ \text{Ø}& \text{otherwise.}\end{cases} \]
It is then clear that the conditions for each set to evaluate to $\text{pt}$ (up to isomorphism) are equivalent, implying that those two sets are isomorphic.