Let $\mathbb{C}$ be a logic. Categories in $\mathbb{C}$ are types with self-relations, and these form a richer logic which we call $\mathrm{Cat}[\mathbb{C}]$.

<aside> ❔ In category theory, what we call “categories” are called monads. Some may have heard of the functional concept of monad, in programming, but ours is the relational concept of monad.

</aside>

Category

A category in $\mathbb{C}$ is a type $\underline{\mathrm{C}}$ and a self-relation $\mathrm{C}: \underline{\mathrm{C}}\,|\, \underline{\mathrm{C}}$

which gives for each pair of elements $\mathrm{a,b}:\underline{\mathrm{C}}$ a relation $\mathrm{C(a,b)}:\mathbb{V}$, and these have composition and identity: inferences

$\mathrm{comp:C(a,b) \circ C(b,c)\to C(a,c)}$

$\mathrm{id:C_\bullet(c=c)\to C(c,c)}$

so that composing is associative

$(f\cdot g)\cdot h$

$f\cdot (g\cdot h)$

and unital.

$\mathrm{id.a}\cdot f$

$f\cdot \mathrm{id.a}$

This is called a “monad” in category theory, and in fact virtually every kind of “category” is a monad!

When $\mathbb{C}$ is the logic of set-matrices, a category is a category.

When $\mathbb{C}$ is the logic of distance, a category is a metric space.