Classical.Small.Structures.Lattice¶

Level-fixed Lattice¶

This is the Classical.Small.Structures.Lattice module of the Agda Universal Algebra Library.

Specializes Classical.Structures.Lattice to the common case where the universe level of both the carrier and the equivalence is 0ℓ (i.e., Set-valued carriers with propositional or set-truncated equivalence), mirroring the veneers of Magma, Semigroup, Monoid, etc.

{-# OPTIONS --cubical-compatible --exact-split --safe #-}
module Classical.Small.Structures.Lattice where
open import Agda.Primitive                         using () renaming ( Set to Type )
open import Level                                  using ( 0ℓ ; suc )
open import Relation.Binary.PropositionalEquality  using ( _≡_ )
import Classical.Structures.Lattice as Polymorphic

Lattice : Type (suc 0ℓ)
Lattice = Polymorphic.Lattice 0ℓ 0ℓ

eqsToLattice : (A : Type 0ℓ) (_∧'_ _∨'_ : A → A → A)
  → (∀ a b c → (a ∧' b) ∧' c ≡ a ∧' (b ∧' c))
  → (∀ a b → a ∧' b ≡ b ∧' a)
  → (∀ a → a ∧' a ≡ a)
  → (∀ a b c → (a ∨' b) ∨' c ≡ a ∨' (b ∨' c))
  → (∀ a b → a ∨' b ≡ b ∨' a)
  → (∀ a → a ∨' a ≡ a)
  → (∀ a b → a ∧' (a ∨' b) ≡ a)
  → (∀ a b → (a ∧' b) ∨' a ≡ a)
  → Lattice
eqsToLattice = Polymorphic.eqsToLattice