In binary logic, a predicate on a type $\mathrm{X}$ is a function $P:\mathrm{X}\to \{0,1\}$. So, a predicate on a pair is a matrix of truth values $R:\mathrm{A\times B}\to \{0,1\}$.
Now we open the possibilities: a relation could be
… anything you want! All we have to define is how to compose such a relation, by “matrix multiplication” — then your relations form a logic, a whole universe in which to explore and build and communicate.
Most kinds of predicates are maps $P:\mathrm{A}\to \mathbb{V}$ for some value logic $\mathbb{V}$. So, the “values” of a predicate $P[\mathrm{a}]$ are types in some logic .
This provides a general yet concrete syntax for predicates; and later we explore why so many notions of predicate are such “valuations”.
In binary logic, $\mathbb{V} = \{0\Rightarrow 1\}$ : the logic with one type, relations 0 and 1, and one inference.
Now, there are infinite possible .
Our working example is $\mathbb{V} = \mathrm{Set}$ : one type, relations are sets, and inferences are functions.
In general, a “world” of types and processes forms a category, and a kind of “predicate” forms a bifibered category. But we don’t need to know these concepts yet — we can follow the visual intuition.
A “kind of type” can be drawn as a color, and a “kind of predicate” can be drawn as a string.
<aside> 🌟 As we step out into the multi-verse of logics, we zoom out: because a “kind of type” is a really a category of types, one zoomed-out color contains many colors “inside”. In the same way, one zoomed-out string contains strings.
</aside>
[ picture of a stack of colors bound by a woven braid ]
For each type $\mathrm{A}:\mathbb{A}$, there is a set of predicates of $\mathrm{A}$, written $\mathcal{P}[\mathrm{A}]$. This is drawn by writing “” in the colored area of $\mathbb{A}$. We can then pick a specific predicate $P$ on this .
Then, picking a specific element $\mathrm{a}$ of $\mathrm{A}$ determines a value of the predicate $P[\mathrm{a}]:\mathbb{V}$. If the context is understood, the syntax on the left can be interpreted as the more explicit syntax on the right.
