---
layout: default
file: "src/Examples/Classical/Lattices/L2.lagda.md"
title: "Examples.Classical.Lattices.L2 module"
date: "2026-05-31"
author: "the agda-algebras development team"
---

### Worked Example: `𝑳𝟚 = (Bool, _∧_, _∨_)` as a Boolean lattice {#examples-classical-lattices-L2}

This is the [Examples.Classical.Lattices.L2][] module of the [Agda Universal Algebra Library][].

`Bool` under meet and join forms the canonical two-element lattice.  Built from
stdlib's `Data.Bool.Properties` lemmas; the only non-trivial step is deriving the
`(a ∧ b) ∨ a ≡ a` form of absorption from stdlib's `∨-absorbs-∧` form via `∨-comm`.

<!--
```agda
{-# OPTIONS --without-K --exact-split --safe #-}
module Examples.Classical.Lattices.L2 where

-- Imports from the Agda Standard Library -------------------------------------
open import Data.Bool             using ( Bool ; _∧_ ; _∨_ )
open import Data.Bool.Properties  using ( ∧-assoc ; ∧-comm ; ∧-idem ; ∨-assoc ; ∨-comm ; ∨-idem )
                                  renaming ( ∧-abs-∨ to ∧-absorbs-∨ ; ∨-abs-∧ to ∨-absorbs-∧ )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl ; trans )

-- Imports from the Agda Universal Algebra Library ----------------------------
open import Classical.Bundles.Lattice           using ( ⟨_⟩ˡᵃ ; ⟪_⟫ˡᵃ )
open import Classical.Small.Structures.Lattice  using ( Lattice ; eqsToLattice )
import Classical.Structures.Lattice as Polymorphic
```
-->

#### Deriving the second absorption equation {#absorbR}

Our `eqsToLattice` takes the second absorption equation in the form `(a ∧ b) ∨ a ≡ a`
(per `Th-Lattice absorbʳ = AbsorbsRight ∧-Op ∨-Op refl refl 0F 1F`); stdlib's
`Data.Bool.Properties.∨-absorbs-∧` is `a ∨ (a ∧ b) ≡ a`.  One `∨-comm` step bridges them.

```agda
Bool-absorbʳ : ∀ a b → (a ∧ b) ∨ a ≡ a
Bool-absorbʳ a b = trans (∨-comm (a ∧ b) a) (∨-absorbs-∧ a b)
```

#### The lattice `𝑳𝟚 = (Bool, _∧_, _∨_)` {#bool-lattice}

`𝑳𝟚` hands `eqsToLattice` the carrier, both operations, and the eight lattice
equations: six stdlib lemmas verbatim, stdlib's `∧-absorbs-∨`, and the derived
`Bool-absorbʳ`.

```agda
𝑳𝟚 : Lattice
𝑳𝟚 = eqsToLattice Bool _∧_ _∨_
  ∧-assoc ∧-comm ∧-idem ∨-assoc ∨-comm ∨-idem ∧-absorbs-∨ Bool-absorbʳ
```

#### Acceptance checks {#acceptance}

The `Lattice-Op` accessors interpret to stdlib's `Bool._∧_` and `Bool._∨_` on the
nose: no opacity from `eqsToLattice`, from the factoring through `opsToBareLattice`,
or from `Curry₂` wrapping; discharged by `refl`.

```agda
open Polymorphic.Lattice-Op 𝑳𝟚 renaming ( _∧_ to _∙∧_ ; _∨_ to _∙∨_ )

∙∧-is-∧-la : ∀ (a b : Bool) → a ∙∧ b ≡ a ∧ b
∙∧-is-∧-la a b = refl

∙∨-is-∨-la : ∀ (a b : Bool) → a ∙∨ b ≡ a ∨ b
∙∨-is-∨-la a b = refl
```

#### Round-trip through `Algebra.Lattice.Bundles.Lattice` {#roundtrip}

The bundle bridge round-trips on `Bool-lattice` pointwise on both operations.
Both directions reduce by `pair a b 0F ⇉ a` and `pair a b 1F ⇉ b`, so
propositional `refl` discharges the obligation at the curried form
(per [ADR-002 v2](../../docs/adr/002-classical-layer-design.md) §6).

```agda
open Polymorphic.Lattice-Op ⟪ ⟨ 𝑳𝟚 ⟩ˡᵃ ⟫ˡᵃ using ()
  renaming ( _∧_ to _∙∧'_ ; _∨_ to _∙∨'_ )

roundtrip-∧-la : ∀ (a b : Bool) → a ∙∧' b ≡ a ∧ b
roundtrip-∧-la a b = refl

roundtrip-∨-la : ∀ (a b : Bool) → a ∙∨' b ≡ a ∨ b
roundtrip-∨-la a b = refl
```

This closes the third bullet of the M3-7 acceptance criteria.