Skip to content

Examples.Classical.Lattices

Worked examples of lattices

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

Barrel for the worked Lattice examples under Examples/Classical/Lattices/. Each submodule is the home of one concrete lattice.

  • L2 is the two-element Boolean lattice.
  • L2Distributive is the two-element Boolean lattice as a DistributiveLattice.
  • L3Heyting is the three-element chain as a Heyting algebra.
  • FreeLattice3 is the free lattice on three generators, in which Whitman's procedure decides inequalities by evaluation.
{-# OPTIONS --without-K --exact-split --safe #-}

module Examples.Classical.Lattices where

open import Examples.Classical.Lattices.L2
open import Examples.Classical.Lattices.L2Distributive
open import Examples.Classical.Lattices.L3Heyting
open import Examples.Classical.Lattices.FreeLattice3