8.1.1 Foundations

Let $A$ and $B$ be sets.

A relation $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ from $A$ to $B$1,2 is equivalently:

  1. 1.

    A subset $R$ of $A\times B$.

  2. 2.

    A function from $A\times B$ to $\{ \mathsf{true},\mathsf{false}\} $.

  3. 3.

    A function from $A$ to $\mathcal{P}\webleft (B\webright )$.

  4. 4.

    A function from $B$ to $\mathcal{P}\webleft (A\webright )$.

  5. 5.

    A cocontinuous morphism of posets from $\webleft (\mathcal{P}\webleft (A\webright ),\subset \webright )$ to $\webleft (\mathcal{P}\webleft (B\webright ),\subset \webright )$.

  6. 6.

    A continuous morphism of posets from $\webleft (\mathcal{P}\webleft (B\webright ),\supset \webright )$ to $\webleft (\mathcal{P}\webleft (A\webright ),\supset \webright )$.


  1. 1Further Terminology: Also called a multivalued function from $A$ to $B$.
  2. 2Further Terminology: When $A=B$, we also call $R\subset A\times A$ a relation on $A$.
Proof of the Equivalences in Definition 8.1.1.1.1.

We may think of a relation $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ as a function from $A$ to $B$ that is multivalued, assigning to each element $a$ in $A$ a set $R\webleft (a\webright )$ of elements of $B$, thought of as the set of values of $R$ at $a$.

Note that this includes also the possibility of $R$ having no value at all on a given $a\in A$ when $R\webleft (a\webright )=\text{Ø}$.

Another way of stating the equivalence between Item 1, Item 2, Item 3, Item 4, and Item 5 of Definition 8.1.1.1.1 is by saying that we have bijections of sets

\begin{align*} \left\{ \text{relations from $A$ to $B$}\right\} & \cong \mathcal{P}\webleft (A\times B\webright )\\ & \cong \mathsf{Sets}\webleft (A\times B,\{ \mathsf{true},\mathsf{false}\} \webright )\\ & \cong \mathsf{Sets}\webleft (A,\mathcal{P}\webleft (B\webright )\webright )\\ & \cong \mathsf{Sets}\webleft (B,\mathcal{P}\webleft (A\webright )\webright )\\ & \cong \mathsf{Pos}^{\style {display: inline-block; transform: rotate(180deg)}{\mathcal{C}}\mkern -2.5mu}\webleft (\mathcal{P}\webleft (A\webright ),\mathcal{P}\webleft (B\webright )\webright )\\ & \cong \mathsf{Pos}^{\mathcal{C}}\webleft (\mathcal{P}\webleft (B\webright ),\mathcal{P}\webleft (A\webright )\webright ) \end{align*}

natural in $A,B\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}\webright )$, where $\mathcal{P}\webleft (A\webright )$ and $\mathcal{P}\webleft (B\webright )$ are endowed with the poset structure given by inclusion.

Proof of the Equivalences in Definition 8.1.1.1.1.

We claim that Item 1, Item 2, Item 3, Item 4, and Item 5 are indeed equivalent:

  • Item 1$\iff $Item 2: This is a special case of Chapter 4: Constructions With Sets, Item 2 and Item 3 of Proposition 4.5.1.1.4.

  • Item 2$\iff $Item 3: This follows from the bijections

    \begin{align*} \mathsf{Sets}\webleft (A\times B,\{ \mathsf{true},\mathsf{false}\} \webright ) & \cong \mathsf{Sets}\webleft (A,\mathsf{Sets}\webleft (B,\{ \mathsf{true},\mathsf{false}\} \webright )\webright )\\ & \cong \mathsf{Sets}\webleft (A,\mathcal{P}\webleft (B\webright )\webright ), \end{align*}

    where the last bijection is from Chapter 4: Constructions With Sets, Item 2 and Item 3 of Proposition 4.5.1.1.4.

  • Item 2$\iff $Item 4: This follows from the bijections

    \begin{align*} \mathsf{Sets}\webleft (A\times B,\{ \mathsf{true},\mathsf{false}\} \webright ) & \cong \mathsf{Sets}\webleft (B,\mathsf{Sets}\webleft (B,\{ \mathsf{true},\mathsf{false}\} \webright )\webright )\\ & \cong \mathsf{Sets}\webleft (B,\mathcal{P}\webleft (A\webright )\webright ), \end{align*}

    where again the last bijection is from Chapter 4: Constructions With Sets, Item 2 and Item 3 of Proposition 4.5.1.1.4.

  • Item 2$\iff $Item 5: This follows from the universal property of the powerset $\mathcal{P}\webleft (X\webright )$ of a set $X$ as the free cocompletion of $X$ via the characteristic embedding

    \[ \chi _{X} \colon X \hookrightarrow \mathcal{P}\webleft (X\webright ) \]

    of $X$ into $\mathcal{P}\webleft (X\webright )$, as in Chapter 4: Constructions With Sets, Proposition 4.4.5.1.1. In particular, the bijection

    \[ \mathsf{Sets}\webleft (A,\mathcal{P}\webleft (B\webright )\webright )\cong \mathsf{Pos}^{\style {display: inline-block; transform: rotate(180deg)}{\mathcal{C}}\mkern -2.5mu}\webleft (\mathcal{P}\webleft (A\webright ),\mathcal{P}\webleft (B\webright )\webright ) \]

    is given by extending each $f\colon A\to \mathcal{P}\webleft (B\webright )$ in $\mathsf{Sets}\webleft (A,\mathcal{P}\webleft (B\webright )\webright )$ from $A$ to all of $\mathcal{P}\webleft (A\webright )$ by taking its left Kan extension along $\chi _{X}$, recovering the direct image function $f_{!}\colon \mathcal{P}\webleft (A\webright )\to \mathcal{P}\webleft (B\webright )$ of $f$ of Chapter 4: Constructions With Sets, Definition 4.6.1.1.1.

  • Item 5$\iff $Item 6: Omitted.

This finishes the proof.

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

  1. 1.

    We write $\mathrm{Rel}\webleft (A,B\webright )$ for the set of relations from $A$ to $B$.

  2. 2.

    We write $\mathbf{Rel}\webleft (A,B\webright )$ for the sub-poset of $\webleft (\mathcal{P}\webleft (A\times B\webright ),\subset \webright )$ spanned by the relations from $A$ to $B$.

  3. 3.

    Given $a\in A$ and $b\in B$, we write $a\sim _{R}b$ to mean $\webleft (a,b\webright )\in R$.

  4. 4.

    When viewing $R$ as a function

    \[ R\colon A\times B\to \{ \mathsf{t},\mathsf{f}\} , \]

    we write $R^{b}_{a}$ for the value of $R$ at $\webleft (a,b\webright )$.1


  1. 1The choice to write $R^{b}_{a}$ in place of $R^{a}_{b}$ is to keep the notation consistent with the notation we will later employ for profunctors in Unresolved reference.

Let $A$ and $B$ be sets and let $R,S\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ be relations.

  1. 1.

    End Formula for the Set of Inclusions of Relations. We have

    \[ \operatorname {\mathrm{Hom}}_{\mathbf{Rel}\webleft (A,B\webright )}\webleft (R,S\webright )\cong \int _{a\in A}\int _{b\in B}\operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (R^{b}_{a},S^{b}_{a}\webright ). \]

Item 1: End Formula for the Set of Inclusions of Relations
Unwinding the expression inside the end on the right hand side, we have

\[ \int _{a\in A}\int _{b\in B}\operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (R^{b}_{a},S^{b}_{a}\webright )\cong \begin{cases} \mathrm{pt}& \text{if, for each $a\in A$ and each $b\in B$,}\\ & \text{we have $\operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (R^{b}_{a},S^{b}_{a}\webright )\cong \mathrm{pt}$}\\ \text{Ø}& \text{otherwise.}\end{cases} \]

Since we have $\operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (R^{b}_{a},S^{b}_{a}\webright )=\left\{ \mathsf{true}\right\} \cong \mathrm{pt}$ exactly when $R^{b}_{a}=\mathsf{false}$ or $R^{b}_{a}=S^{b}_{a}=\mathsf{true}$, we get

\[ \int _{a\in A}\int _{b\in B}\operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (R^{b}_{a},S^{b}_{a}\webright )\cong \begin{cases} \mathrm{pt}& \text{if, for each $a\in A$ and each $b\in B$,}\\ & \text{if $a\sim _{R}b$, then $a\sim _{S}b$,}\\ \text{Ø}& \text{otherwise.}\end{cases} \]

On the left hand-side, we have

\[ \operatorname {\mathrm{Hom}}_{\mathbf{Rel}\webleft (A,B\webright )}\webleft (R,S\webright )\cong \begin{cases} \mathrm{pt}& \text{if $R\subset S$,}\\ \text{Ø}& \text{otherwise.}\end{cases} \]

Since $\webleft (a\sim _{R}b\implies a\sim _{S}b\webright )$ iff $R\subset S$, the two sets above are isomorphic. This finishes the proof.


Noticed something off, or have any comments? Feel free to reach out!


You can also use the contact form below: