Preorder as Bool-Category

Textbook Description

Example 2.31. As we shall see in the next subsection, from every preorder we can construct a Bool-category, and vice versa. So, to get a feel for V-categories, let us consider the preorder generated by the Hasse diagram (2.17).

p -> q
|    |
v    v
r -> s
     |
     v
     t

How does this correspond to a Bool-category X? Well, the objects of X are simply the elements of the preorder, i.e. Ob(X) = {p, q, r, s, t}. Next, for every pair of objects (x, y) we need an element of B = {false, true}: simply take true if x ≤ y, and false otherwise. So, for example, since s ≤ t and t ≰ s, we have X(s, t) = true and X(t, s) = false. Recalling from Example 2.12 that the monoidal unit I of Bool is true, it’s straightforward to check that this obeys both (a) and (b), so we have a Bool-category.

In general, it’s sometimes convenient to represent a V-category X with a square matrix. The rows and columns of the matrix correspond to the objects of X, and the (x, y)th entry is simply the hom-object X(x, y). So, for example, the above preorder in Eq. (2.17) can be represented by the matrix:

· ≤ · p q r s t
p   ⊤ ⊤ ⊤ ⊤ ⊤
q   ⊥ ⊤ ⊥ ⊤ ⊤
r   ⊥ ⊥ ⊤ ⊤ ⊤
s   ⊥ ⊥ ⊥ ⊤ ⊤
t   ⊥ ⊥ ⊥ ⊥ ⊤

Agda Setup

module examples.chapter2.PreorderAsBoolCategory where

open import definitions.chapter1.Preorder using (Preorder; IsPreorder)
open import definitions.chapter2.SymmetricMonoidalPreorder
  using (SymmetricMonoidalStructure; SymmetricMonoidalPreorder)
open import definitions.chapter2.VCategory using (VCategory)
open import Data.Bool using (Bool; true; false; _∧_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; inspect; [_])
open Relation.Binary.PropositionalEquality using (subst; sym; trans)

The Preorder

From the Hasse diagram, we have: p ≤ {p,q,r,s,t}, q ≤ {q,s,t}, r ≤ {r,s,t}, s ≤ {s,t}, t ≤ {t}.

-- The five elements of our preorder
data Element : Set where
  p q r s t : Element

-- The ordering relation from the Hasse diagram
data _≤E_ : Element → Element → Set where
  p≤p : p ≤E p
  p≤q : p ≤E q
  p≤r : p ≤E r
  p≤s : p ≤E s
  p≤t : p ≤E t
  q≤q : q ≤E q
  q≤s : q ≤E s
  q≤t : q ≤E t
  r≤r : r ≤E r
  r≤s : r ≤E s
  r≤t : r ≤E t
  s≤s : s ≤E s
  s≤t : s ≤E t
  t≤t : t ≤E t

-- Reflexivity and transitivity
≤E-refl : ∀ {x : Element} → x ≤E x
≤E-trans : ∀ {x y z : Element} → x ≤E y → y ≤E z → x ≤E z

-- The preorder structure
element-preorder : Preorder

Implementation

Strategy: Verify reflexivity and transitivity by case analysis on all constructors.

≤E-refl {p} = p≤p
≤E-refl {q} = q≤q
≤E-refl {r} = r≤r
≤E-refl {s} = s≤s
≤E-refl {t} = t≤t

≤E-trans p≤p p≤p = p≤p
≤E-trans p≤p p≤q = p≤q
≤E-trans p≤p p≤r = p≤r
≤E-trans p≤p p≤s = p≤s
≤E-trans p≤p p≤t = p≤t
≤E-trans p≤q q≤q = p≤q
≤E-trans p≤q q≤s = p≤s
≤E-trans p≤q q≤t = p≤t
≤E-trans p≤r r≤r = p≤r
≤E-trans p≤r r≤s = p≤s
≤E-trans p≤r r≤t = p≤t
≤E-trans p≤s s≤s = p≤s
≤E-trans p≤s s≤t = p≤t
≤E-trans p≤t t≤t = p≤t
≤E-trans q≤q q≤q = q≤q
≤E-trans q≤q q≤s = q≤s
≤E-trans q≤q q≤t = q≤t
≤E-trans q≤s s≤s = q≤s
≤E-trans q≤s s≤t = q≤t
≤E-trans q≤t t≤t = q≤t
≤E-trans r≤r r≤r = r≤r
≤E-trans r≤r r≤s = r≤s
≤E-trans r≤r r≤t = r≤t
≤E-trans r≤s s≤s = r≤s
≤E-trans r≤s s≤t = r≤t
≤E-trans r≤t t≤t = r≤t
≤E-trans s≤s s≤s = s≤s
≤E-trans s≤s s≤t = s≤t
≤E-trans s≤t t≤t = s≤t
≤E-trans t≤t t≤t = t≤t

element-preorder = record
  { Carrier = Element
  ; _≤_ = _≤E_
  ; isPreorder = record
      { reflexive = ≤E-refl
      ; transitive = ≤E-trans
      }
  }

Bool Symmetric Monoidal Preorder

We define Bool with ordering false ≤ true, monoidal unit true, and monoidal product ∧.

-- The ordering on Bool: false ≤ true
data _≤Bool_ : Bool → Bool → Set where
  false≤false : false ≤Bool false
  false≤true  : false ≤Bool true
  true≤true   : true ≤Bool true

-- Bool is a preorder
≤Bool-refl : ∀ {x : Bool} → x ≤Bool x
≤Bool-trans : ∀ {x y z : Bool} → x ≤Bool y → y ≤Bool z → x ≤Bool z
Bool-preorder : Preorder

-- ∧ satisfies the monoidal structure conditions
∧-monotonic : ∀ {x₁ x₂ y₁ y₂ : Bool} → x₁ ≤Bool y₁ → x₂ ≤Bool y₂ → (x₁ ∧ x₂) ≤Bool (y₁ ∧ y₂)
∧-identityˡ : ∀ {x : Bool} → true ∧ x ≡ x
∧-identityʳ : ∀ {x : Bool} → x ∧ true ≡ x
∧-assoc : ∀ (x y z : Bool) → (x ∧ y) ∧ z ≡ x ∧ (y ∧ z)
∧-comm : ∀ (x y : Bool) → x ∧ y ≡ y ∧ x

-- Bool as a symmetric monoidal preorder
Bool-monoidal-structure : SymmetricMonoidalStructure Bool-preorder
Bool-monoidal : SymmetricMonoidalPreorder

Implementation

Strategy: Verify all properties by case analysis on boolean values.

≤Bool-refl {false} = false≤false
≤Bool-refl {true} = true≤true

≤Bool-trans false≤false false≤false = false≤false
≤Bool-trans false≤false false≤true = false≤true
≤Bool-trans false≤true true≤true = false≤true
≤Bool-trans true≤true true≤true = true≤true

Bool-preorder = record
  { Carrier = Bool
  ; _≤_ = _≤Bool_
  ; isPreorder = record
      { reflexive = ≤Bool-refl
      ; transitive = ≤Bool-trans
      }
  }

∧-monotonic false≤false false≤false = false≤false
∧-monotonic false≤false false≤true = false≤false
∧-monotonic false≤false true≤true = false≤false
∧-monotonic false≤true false≤false = false≤false
∧-monotonic false≤true false≤true = false≤true
∧-monotonic false≤true true≤true = false≤true
∧-monotonic true≤true false≤false = false≤false
∧-monotonic true≤true false≤true = false≤true
∧-monotonic true≤true true≤true = true≤true

∧-identityˡ {false} = refl
∧-identityˡ {true} = refl

∧-identityʳ {false} = refl
∧-identityʳ {true} = refl

∧-assoc false y z = refl
∧-assoc true y z = refl

∧-comm false false = refl
∧-comm false true = refl
∧-comm true false = refl
∧-comm true true = refl

Bool-monoidal-structure = record
  { I = true
  ; _⊗_ = _∧_
  ; monotonicity = ∧-monotonic
  ; left-unit = ∧-identityˡ
  ; right-unit = ∧-identityʳ
  ; associativity = λ {x} {y} {z} → ∧-assoc x y z
  ; symmetry = λ {x} {y} → ∧-comm x y
  }

Bool-monoidal = record
  { preorder = Bool-preorder
  ; structure = Bool-monoidal-structure
  }

The Bool-Category

We construct a Bool-category by defining X(x, y) = true if x ≤ y, false otherwise.

-- The hom-object function
hom : Element → Element → Bool
hom p p = true
hom p q = true
hom p r = true
hom p s = true
hom p t = true
hom q p = false
hom q q = true
hom q r = false
hom q s = true
hom q t = true
hom r p = false
hom r q = false
hom r r = true
hom r s = true
hom r t = true
hom s p = false
hom s q = false
hom s r = false
hom s s = true
hom s t = true
hom t p = false
hom t q = false
hom t r = false
hom t s = false
hom t t = true

-- The identity law: I ≤ X(x, x)
identity-law : ∀ {x : Element} → true ≤Bool hom x x

-- Helper lemmas connecting hom with the ordering
hom-reflects-≤ : ∀ {x y : Element} → hom x y ≡ true → x ≤E y
hom-preserves-≤ : ∀ {x y : Element} → x ≤E y → hom x y ≡ true

-- Helper for the impossible case
hom-trans-true : ∀ {x y z : Element} → hom x y ≡ true → hom y z ≡ true → hom x z ≡ true
hom-trans-true {x} {y} {z} xy≡ yz≡ = hom-preserves-≤ (≤E-trans (hom-reflects-≤ xy≡) (hom-reflects-≤ yz≡))

-- The composition law: X(x, y) ⊗ X(y, z) ≤ X(x, z)
composition-law : ∀ {x y z : Element} → (hom x y ∧ hom y z) ≤Bool hom x z

-- The Bool-category structure
element-Bool-category : VCategory Bool-monoidal

Implementation

Strategy: The identity law holds because hom x x = true for all x (reflexivity). For the composition law, we use helper lemmas to connect hom with the ordering, then leverage transitivity of ≤E instead of exhaustive case analysis.

identity-law {p} = true≤true
identity-law {q} = true≤true
identity-law {r} = true≤true
identity-law {s} = true≤true
identity-law {t} = true≤true

-- hom x y = true if and only if x ≤E y
hom-reflects-≤ {p} {p} refl = p≤p
hom-reflects-≤ {p} {q} refl = p≤q
hom-reflects-≤ {p} {r} refl = p≤r
hom-reflects-≤ {p} {s} refl = p≤s
hom-reflects-≤ {p} {t} refl = p≤t
hom-reflects-≤ {q} {q} refl = q≤q
hom-reflects-≤ {q} {s} refl = q≤s
hom-reflects-≤ {q} {t} refl = q≤t
hom-reflects-≤ {r} {r} refl = r≤r
hom-reflects-≤ {r} {s} refl = r≤s
hom-reflects-≤ {r} {t} refl = r≤t
hom-reflects-≤ {s} {s} refl = s≤s
hom-reflects-≤ {s} {t} refl = s≤t
hom-reflects-≤ {t} {t} refl = t≤t

hom-preserves-≤ p≤p = refl
hom-preserves-≤ p≤q = refl
hom-preserves-≤ p≤r = refl
hom-preserves-≤ p≤s = refl
hom-preserves-≤ p≤t = refl
hom-preserves-≤ q≤q = refl
hom-preserves-≤ q≤s = refl
hom-preserves-≤ q≤t = refl
hom-preserves-≤ r≤r = refl
hom-preserves-≤ r≤s = refl
hom-preserves-≤ r≤t = refl
hom-preserves-≤ s≤s = refl
hom-preserves-≤ s≤t = refl
hom-preserves-≤ t≤t = refl

-- When hom x y ∧ hom y z = true, both x ≤ y and y ≤ z, so x ≤ z by transitivity
-- When hom x y ∧ hom y z = false, we get false ≤Bool hom x z (always true)
composition-law {x} {y} {z} with hom x y in xy≡ | hom y z in yz≡ | hom x z in xz≡
... | false | false | false = false≤false
... | false | false | true  = false≤true
... | false | true  | false = false≤false
... | false | true  | true  = false≤true
... | true  | false | false = false≤false
... | true  | false | true  = false≤true
... | true  | true  | false = absurd (trans (sym (hom-trans-true {x} {y} {z} xy≡ yz≡)) xz≡)
  where
    absurd : ∀ {A : Set} → true ≡ false → A
    absurd ()
... | true  | true  | true = true≤true

element-Bool-category = record
  { Ob = Element
  ; hom = hom
  ; identity = identity-law
  ; composition = composition-law
  }