The Clowder Project

Let $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ be a relation.

1. Functionality I. The assignment $R\mapsto R^{-1}$ defines a function
   \[ \webleft (-\webright )^{-1}\colon \mathrm{Rel}\webleft (A,B\webright ) \to \mathsf{Sets}\webleft (\mathcal{P}\webleft (A\webright ),\mathcal{P}\webleft (B\webright )\webright ). \]
2. Functionality II. The assignment $R\mapsto R^{-1}$ defines a function
   \[ \webleft (-\webright )^{-1}\colon \mathrm{Rel}\webleft (A,B\webright ) \to \mathsf{Pos}\webleft (\webleft (\mathcal{P}\webleft (A\webright ),\subset \webright ),\webleft (\mathcal{P}\webleft (B\webright ),\subset \webright )\webright ). \]
3. Interaction With Identities. For each $A\in \text{Obj}\webleft (\mathsf{Sets}\webright )$, we have¹
   \[ \webleft (\chi _{A}\webright )^{-1}=\text{id}_{\mathcal{P}\webleft (A\webright )}; \]
4. Interaction With Composition. For each pair of composable relations $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ and $S\colon B\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}C$, we have²
   

---

¹That is, the postcomposition

\[ \webleft (\chi _{A}\webright )^{-1}\colon \mathrm{Rel}\webleft (\text{pt},A\webright )\to \mathrm{Rel}\webleft (\text{pt},A\webright ) \]

is equal to $\text{id}_{\mathrm{Rel}\webleft (\text{pt},A\webright )}$.

²That is, we have