Now: given a “kind of predicate” $\mathcal{P}$ over $\mathbb{A}$, we can define a relation $R:\mathrm{A}\,|\, \mathrm{B}$ to be a predicate $R$ of pairs $\mathrm{(a,b):A\times B}$.

matrix.png

This is a matrix indexed by $\mathrm{A\times B}$, with values given by $R$.

| $R:\mathrm{A}\,|\, \mathrm{B}$ | $\mathrm{b:B}$ | $\cdots$ | | --- | --- | --- | | $\mathrm{a:A}$ | $R(\mathrm{a,b})$ | | | $\cdots$ | | |

Ex. In set-valued logic, a relation is a matrix of sets $R(\mathrm{a,b}):\mathrm{Set}$.

So how do we compose relations? Given $R: \mathrm{A}\,|\, \mathrm{B}$ and $S: \mathrm{B}\,|\, \mathrm{C}$,

rel-comp.png

$$ R\circ S = \mathsf{\Sigma}\, \mathrm{b:B}.\; R(-,\mathrm{b}) \circ S(\mathrm{b},-) . $$

There are just two steps:

  1. match the middle variable $\mathrm{b:B}$, and then
  2. sum over the middle variable.

We can visualize this as follows.

mat-comp.png

Identity:

rel-id.png