A relation $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ is functional if, for each $a\in A$, the set $R(a)$ is either empty or a singleton.
Let $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ be a relation.
Proof of Proposition 10.1.1.1.2.
Item 1: Characterisations
We claim that Item 1a and Item 1b are indeed equivalent:
-
•
Item 1a$\implies $Item 1b: Let $(b,b')\in B\times B$. We need to show that
\[ [R\mathbin {\diamond }R^{\dagger }](b,b')\preceq _{\{ \mathsf{t},\mathsf{f}\} }\chi _{B}(b,b'), \]i.e. that if there exists some $a\in A$ such that $b\sim _{R^{\dagger }}a$ and $a\sim _{R}b'$, then $b=b'$. But since $b\sim _{R^{\dagger }}a$ is the same as $a\sim _{R}b$, we have both $a\sim _{R}b$ and $a\sim _{R}b'$ at the same time, which implies $b=b'$ since $R$ is functional.
-
•
Item 1b$\implies $Item 1a: Suppose that we have $a\sim _{R}b$ and $a\sim _{R}b'$ for $b,b'\in B$. We claim that $b=b'$:
-
•
Since $a\sim _{R}b$, we have $b\sim _{R^{\dagger }}a$.
-
•
Since $R\mathbin {\diamond }R^{\dagger }\subset \chi _{B}$, we have
\[ [R\mathbin {\diamond }R^{\dagger }](b,b')\preceq _{\{ \mathsf{t},\mathsf{f}\} }\chi _{B}(b,b'), \]and since $b\sim _{R^{\dagger }}a$ and $a\sim _{R}b'$, it follows that $[R\mathbin {\diamond }R^{\dagger }](b,b')=\mathsf{true}$, and thus $\chi _{B}(b,b')=\mathsf{true}$ as well, i.e. $b=b'$.
-
•
This finishes the proof.
