Examples.Setoid.SubalgebraLattice

Worked example: the subalgebra lattice of a two-element algebra

This is the Examples.Setoid.SubalgebraLattice module of the Agda Universal Algebra Library.

We exercise Setoid.Subalgebras.CompleteLattice on the two-element algebra 𝟚 in the empty signature (no operations), whose carrier is Bool. Since there are no operations, every subset of the carrier is closed under the operations (vacuously), so the subuniverses of 𝟚 are exactly the four subsets of a two-element set: Sub 𝟚 is the Boolean lattice 2² (the diamond), with bottom ∅, top {true, false}, and the two incomparable singletons in between.

We instantiate the Lattice, BoundedLattice, and CompleteLattice bundles for 𝟚 and verify the lattice is nontrivial by proving ⊤ ⋬ ⊥ (the full subuniverse is not contained in the empty one).

{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Examples.Setoid.SubalgebraLattice where

-- Imports from Agda and the Agda Standard Library ------------------------------
open import Data.Bool.Base    using ( Bool ; true )
open import Data.Empty        using ( ⊥ )
open import Data.Product      using ( _,_ )
open import Data.Unit.Base    using ( tt )
open import Function          using ( Func )
open import Level             using ( 0ℓ ; Lift ; lift ; lower )
open import Relation.Binary   using ( Setoid )
open import Relation.Binary.PropositionalEquality as ≡ using ( _≡_ )
open import Relation.Nullary  using ( ¬_ )

-- Imports from the Agda Universal Algebra Library ------------------------------
open import Overture using ( Signature )

open Func renaming ( to to _⟨$⟩_ )

The empty signature and the two-element algebra 𝟚

𝑆₀ : Signature 0ℓ 0ℓ
𝑆₀ = ⊥ , λ ()

open import Setoid.Algebras {𝑆 = 𝑆₀}  using ( Algebra )
open import Setoid.Signatures         using ( ⟨_⟩ )

-- The two-element algebra: carrier Bool with ≡, and no operations to interpret.
𝟚 : Algebra 0ℓ 0ℓ
𝟚 = record { Domain = ≡.setoid Bool ; Interp = interp }
  where
  interp : Func (⟨ 𝑆₀ ⟩ (≡.setoid Bool)) (≡.setoid Bool)
  interp ⟨$⟩ (() , _)
  cong interp {() , _}

Instantiating the bundles

With base level ℓ₀ = 0ℓ the absorbing level L is 0ℓ, so the subalgebra lattice of 𝟚 lives on Subᴸ. We open Sublattice 𝟚 0ℓ to bring the order, operations, bounds, and bundles into scope specialized to 𝟚 — so we may write B ≤ C rather than _≤_ 𝟚 0ℓ B C. All three bundles type-check.

open import Setoid.Subalgebras.CompleteLattice {𝑆 = 𝑆₀} using ( module Sublattice )
open Sublattice 𝟚 0ℓ

Nontriviality: ⊤ ⋬ ⊥

The empty subuniverse ∅ is a genuine subuniverse of 𝟚 (vacuously, as 𝑆₀ has no operations). If we had ⊤ ≤ ⊥, then since ⊥ is the least subuniverse it is below ∅, so true ∈ ⊤ would force true ∈ ∅ — impossible.

-- The empty subuniverse, as an element of Subᴸ.
∅ˢ : Subᴸ
∅ˢ = (λ _ → Lift 0ℓ ⊥) , λ ()

Sub𝟚-nontrivial : ¬ ( 1ˢ ≤ 0ˢ )
Sub𝟚-nontrivial 1≤0 = lower (0ˢ-minimum ∅ˢ (1≤0 {true} (lift tt)))