Bool (Monoidal Preorder)

definition example

$$\mathbf{Bool}:=(\mathbb{B},\le ,\mathsf{true},\wedge )$$

is the Symmetric Monoidal Preorder on the Booleans with monoidal unit $\mathsf{true}$ and monoidal product AND. Identifying $\mathsf{false}=0$, $\mathsf{true}=1$, $\wedge$ is multiplication:

$\wedge$	$\mathsf{false}$	$\mathsf{true}$
$\mathsf{false}$	$\mathsf{false}$	$\mathsf{false}$
$\mathsf{true}$	$\mathsf{false}$	$\mathsf{true}$

Sources: 7 Sketches Example 2.27, Exercises 2.29, 2.84, 2.93, Theorem 2.49; DaoFP §20.1 (“the monoidal walking arrow”); Kittenlab Lecture 14.

As a base of enrichment. $\mathbf{Bool}$-categories are exactly preorders (Preorders are Bool-Categories): the underlying set says “getting from $a$ to $b$ is a true/false question”; the unit $\mathsf{true}$ says “you can always get from $a$ to $a$”; the product $\wedge$ says “if you can get from $a$ to $b$ AND from $b$ to $c$ then from $a$ to $c$”; the “if–then” is the order $\le$. DaoFP calls $\mathbb{B}$ the walking arrow $\mathsf{False}\to \mathsf{True}$ made monoidal by $\mathsf{True}\otimes \mathsf{True}=\mathsf{True}$, everything else $\mathsf{False}$.

Properties. $\mathbf{Bool}$ is monoidal closed with hom-element implication $v\Rightarrow w$ (7S Exercise 2.84) and is a Quantale with joins given by OR (7S Exercise 2.93); the empty join is $\mathsf{false}$ (7S Exercise 2.92). Its identity $\mathbf{Bool}$-matrix is the usual identity with $\mathsf{true}$ on the diagonal.

The other structure. $(\mathbb{B},\le ,\mathsf{false},\vee )$ is also a symmetric monoidal preorder (7S Exercise 2.29), but it is not closed (Example 2.85): closedness would need $a\vee \mathsf{true}\le \mathsf{false}⟺a\le (\mathsf{true}⊸\mathsf{false})$; for $a=\mathsf{false}$ the right side always holds while the left side $\mathsf{true}\le \mathsf{false}$ fails.

Maps. Monoidal monotones $\mathbf{Bool}\to \mathbf{Cost}$ ($\mathsf{false}\mapsto \infty$, $\mathsf{true}\mapsto 0$) and $\mathbf{Cost}\to \mathbf{Bool}$ (“is $x=0$?”, “is $x<\infty$?”) connect preorders and metric spaces via Change of Base. $\mathbf{Bool}$-profunctors are feasibility relations (Chapter 4).

JuliaLeanHaskell

Docs: Kittenlab Lecture 14

Builds on: Preorder (Preorder) — run that note’s Julia code first.

struct BoolPre <: Preorder{Bool} end
leq(::BoolPre, a::Bool, b::Bool) = a <= b       # false ≤ true
otimes(::BoolPre, a, b) = a && b
munit(::BoolPre) = true
hom(::BoolPre, v, w) = !v || w                  # v ⊸ w = (v ⇒ w)
join(::BoolPre, a, b) = a || b

-- Bool is a Boolean algebra: ⊓ = and, ⊔ = or, ⇨ = implication (the closed structure)
example : BooleanAlgebra Bool := inferInstance
example (a v w : Bool) : (a ⊓ v ≤ w) ↔ (a ≤ v ⇨ w) := le_himp_iff
-- Prop is the "large" version: a Heyting algebra with → as internal hom
example (a v w : Prop) : (a ∧ v → w) ↔ (a → v → w) := ⟨fun h ha hv => h ⟨ha, hv⟩, fun h ⟨ha, hv⟩ => h ha hv⟩

import Data.Monoid (All(..))
-- (Bool, &&, True) is the monoid All; with False <= True it is the monoidal preorder Bool
instance Preorder All where leq (All a) (All b) = a <= b
instance MonoidalPreorder All
 
implies :: Bool -> Bool -> Bool   -- the hom-element v ⊸ w
implies v w = not v || w