The Clowder Project

The inverse of $R$¹ is the relation $\smash {R^{\dagger }}$ defined as follows:

• Viewing relations as subsets, we define
  \[ R^{\dagger } \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ \webleft (b,a\webright )\in B\times A\ \middle |\ \text{we have $b\sim _{R}a$}\webright\} . \]

• Viewing relations as functions $A\times B\to \{ \mathsf{true},\mathsf{false}\} $, we define
  \[ {\webleft [R^{\dagger }\webright ]}{}^{b}_{a} \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}R^{a}_{b} \]

  for each $\webleft (b,a\webright )\in B\times A$.

• Viewing relations as functions $A\to \mathcal{P}\webleft (B\webright )$, we define
  \begin{align*} \webleft [R^{\dagger }\webright ]\webleft (b\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}R^{\dagger }\webleft (\webleft\{ b\webright\} \webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ a\in A\ \middle |\ b\in R\webleft (a\webright )\webright\} \end{align*}

  for each $b\in B$, where $R^{\dagger }\webleft (\webleft\{ b\webright\} \webright )$ is the fibre of $R$ over $\webleft\{ b\webright\} $.