Preorders are Bool-Categories

theorem proof

Theorem 2.49. There is a one-to-one correspondence between preorders and $\mathbf{Bool}$-categories.

Sources: 7 Sketches Theorem 2.49, Example 2.47, 2.70, Remark 2.71, Exercise 2.50; DaoFP §20.1 (“Preorders”).

“Here we find ourselves in the primordial ooze”: preorders are $\mathbf{Bool}$-categories, while $\mathbf{Bool}$ is itself a preorder — every preorder, including $\mathbf{Bool}$, is enriched in $\mathbf{Bool}$.

Proof. A $\mathbf{Bool}$-category $\mathcal{X}$ is a set $\mathrm{Ob}(\mathcal{X})$ with, for each $x,y$, a truth value $\mathcal{X}(x,y)$. Declare $x\le y$ iff $\mathcal{X}(x,y)=\mathsf{true}$. Axiom (a), $\mathsf{true}\le \mathcal{X}(x,x)$, forces $\mathcal{X}(x,x)=\mathsf{true}$: reflexivity. Axiom (b), $\mathcal{X}(x,y)\wedge \mathcal{X}(y,z)\le \mathcal{X}(x,z)$, has force only when both are $\mathsf{true}$, and then forces $\mathcal{X}(x,z)=\mathsf{true}$: transitivity. Conversely (Example 2.47) a preorder gives a $\mathbf{Bool}$-category with $\mathcal{X}(x,y)=\mathsf{true}$ iff $x\le y$. The two constructions are inverse (7S Exercise 2.50). $■$

DaoFP’s version: in the monoidal walking arrow, composition $\mathcal{C}(b,c)\otimes \mathcal{C}(a,b)\to \mathcal{C}(a,c)$ cannot go from $\mathsf{True}$ to $\mathsf{False}$, hence $b\le c\wedge a\le b\Rightarrow a\le c$; identity $j_a:\mathsf{True}\to \mathcal{C}(a,a)$ forces $a\le a$. Cycles $a\le b\le a$ with $a\ne b$ are allowed.

Extension to maps (Example 2.70): monotone maps are exactly $\mathbf{Bool}$-functors, since $\mathcal{X}(x_1,x_2)\le \mathcal{Y}(F{x}_1,F{x}_2)$ in $\mathbb{B}$ says ”$x_1\le x_2$ implies $F{x}_1\le F{x}_2$“. This gives an Equivalence of Categories $\mathbf{Preord}\simeq \mathbf{Bool}\text{-}\mathbf{Cat}$ (Remark 2.71, 3.59). The Product Preorder is the $\mathbf{Bool}$-product, and categories are to $\mathbf{Set}$ as preorders are to $\mathbf{Bool}$.