The Clowder Project

\begin{align*} R^{\dagger } & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ a\in A\ \middle |\ b\in R(a)\right\} \\ & \subset \left\{ a\in A\ \middle |\ b\in S(a)\right\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}S^{\dagger }. \end{align*}

\begin{align*} \operatorname {Dom}(R^{\dagger }) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ b\in B\ \middle |\ \text{$b\sim _{R^{\dagger }}a$ for some $a\in A$}\right\} \\ & = \left\{ b\in B\ \middle |\ \text{$a\sim _{R}b$ for some $a\in A$}\right\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\mathrm{Im}(R) \end{align*}

\begin{align*} \mathrm{Im}(R^{\dagger }) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ a\in A\ \middle |\ \text{$b\sim _{R^{\dagger }}a$ for some $b\in B$}\right\} \\ & = \left\{ a\in A\ \middle |\ \text{$a\sim _{R}b$ for some $b\in B$}\right\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\operatorname {Dom}(R). \end{align*}

\begin{align*} (S\mathbin {\diamond }R)^{\dagger } & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ (c,a)\in C\times A\ \middle |\ c\sim _{(S\mathbin {\diamond }R)^{\dagger }}a\right\} \\ & = \left\{ (c,a)\in C\times A\ \middle |\ a\sim _{S\mathbin {\diamond }R}c\right\} \\ & = \left\{ (c,a)\in C\times A\ \middle |\ \begin{aligned} & \text{there exists some $b\in B$ such}\\ & \text{that $a\sim _{R}b$ and $b\sim _{S}c$}\\ \end{aligned} \right\} \\ & = \left\{ (c,a)\in C\times A\ \middle |\ \begin{aligned} & \text{there exists some $b\in B$ such}\\ & \text{that $b\sim _{R^{\dagger }}a$ and $c\sim _{S^{\dagger }}b$}\\ \end{aligned} \right\} \\ & = \left\{ (c,a)\in C\times A\ \middle |\ \begin{aligned} & \text{there exists some $b\in B$ such}\\ & \text{that $c\sim _{S^{\dagger }}b$ and $b\sim _{R^{\dagger }}a$ }\\ \end{aligned} \right\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}R^{\dagger }\mathbin {\diamond }S^{\dagger }. \end{align*}

\begin{align*} (S\mathbin {\square }R)^{\dagger } & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ (c,a)\in C\times A\ \middle |\ c\sim _{(S\mathbin {\square }R)^{\dagger }}a\right\} \\ & = \left\{ (c,a)\in C\times A\ \middle |\ a\sim _{S\mathbin {\square }R}c\right\} \\ & = \left\{ (c,a)\in C\times A\ \middle |\ \begin{aligned} & \text{for each $b\in B$, we have}\\ & \text{$a\sim _{R}b$ or $b\sim _{S}c$}\\ \end{aligned} \right\} \\ & = \left\{ (c,a)\in C\times A\ \middle |\ \begin{aligned} & \text{for each $b\in B$, we have}\\ & \text{$b\sim _{R^{\dagger }}a$ or $c\sim _{S^{\dagger }}b$}\\ \end{aligned} \right\} \\ & = \left\{ (c,a)\in C\times A\ \middle |\ \begin{aligned} & \text{for each $b\in B$, we have}\\ & \text{$c\sim _{S^{\dagger }}b$ or $b\sim _{R^{\dagger }}a$}\\ \end{aligned} \right\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}R^{\dagger }\mathbin {\square }S^{\dagger }. \end{align*}

\begin{align*} (R^{\dagger })^{\dagger } & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ (a,b)\in A\times B\ \middle |\ b\sim _{R^{\dagger }}a\right\} \\ & = \left\{ (a,b)\in A\times B\ \middle |\ a\sim _{R}b\right\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}R. \end{align*}

\begin{align*} \Delta ^{\dagger }_{A} & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ (a,b)\in A\times A\ \middle |\ a\sim _{\Delta _{A}}b\right\} \\ & = \left\{ (a,b)\in A\times A\ \middle |\ a=b\right\} \\ & = \Delta _{A}. \end{align*}

\begin{align*} \nabla ^{\dagger }_{A} & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ (a,b)\in A\times A\ \middle |\ a\sim _{\nabla _{A}}b\right\} \\ & = \left\{ (a,b)\in A\times A\ \middle |\ a\neq b\right\} \\ & = \nabla _{A}. \end{align*}