We can share a language for all kinds of thinking, if we determine the basic structure of a “kind of thinking”, and understand the language of these structures. So, we proceed from the introduction: what is the structure of a logic?
We can understand this by each dimension: type and process, relation and inference.
Types form a category, and processes form a profunctor. So the language of categories, of objects and morphisms, forms dimensions 0 and V of logic.
Now, relations form a category as well; yet a relation depends on a pair of types, and an inference depends on a pair of processes. So, the language of matrices of categories and matrices of profunctors forms the dimensions H and VH of logic. This is the middle column below.
| type category $\mathbb{X}:\mathrm{Cat}$ | relation span category $\mathbb{X}\leftarrow \mathcal{Q}\to \mathbb{Y}$ | type category $\mathbb{Y}:\mathrm{Cat}$ | | --- | --- | --- | | process profunctor $f:\mathrm{Prof}$ | inference span profunctor $f\Leftarrow i\Rightarrow g$ | process profunctor $g:\mathrm{Prof}$ | | type category $\mathbb{X}:\mathrm{Cat}$ | relation span category $\mathbb{A}\leftarrow \mathcal{R}\to \mathbb{B}$ | type category $\mathbb{Y}:\mathrm{Cat}$ |
In this way, the language of dependent categories can be understood as metalogic: each span profunctor is a kind of thinking, and each span transformation is... well, a way to transform one kind of thinking into another.
Because a span profunctor is a system of inference, it can be imagined as a bead. Now, the third dimension is inner to outer: a span transformation is a flow or a bead within a bead. We define the three-dimensional visual language of dependent categories.