We have an isomorphism of categories
\[ \mathrm{Rel}\cong \mathsf{FreeAlg}_{\mathcal{P}_{!}}\webleft (\mathsf{Sets}\webright ), \]
where $\mathcal{P}_{!}$ is the powerset monad of 
, .
8.4.14 $\mathsf{Rel}$ as a Category of Free Algebras
Proof of Proposition 8.4.14.1.1.
Omitted.
