------------------------------------------------------------------------ -- The Agda standard library -- -- Some derivable properties of semilattices ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} open import Algebra.Lattice.Bundles using (Semilattice) module Algebra.Lattice.Properties.Semilattice {c ℓ} (L : Semilattice c ℓ) where open import Relation.Binary.Bundles using (Poset) import Relation.Binary.Lattice as B import Relation.Binary.Properties.Poset as PosetProperties open Semilattice L renaming (_∙_ to _∧_) open import Relation.Binary.Reasoning.Setoid setoid import Relation.Binary.Construct.NaturalOrder.Left _≈_ _∧_ as LeftNaturalOrder ------------------------------------------------------------------------ -- Every semilattice can be turned into a poset via the left natural -- order. poset : Poset c ℓ ℓ poset = LeftNaturalOrder.poset isSemilattice open Poset poset using (_≤_; _≥_; isPartialOrder) open PosetProperties poset using (≥-isPartialOrder) ------------------------------------------------------------------------ -- Every algebraic semilattice can be turned into an order-theoretic one. ∧-isOrderTheoreticMeetSemilattice : B.IsMeetSemilattice _≈_ _≤_ _∧_ ∧-isOrderTheoreticMeetSemilattice = record { isPartialOrder = isPartialOrder ; infimum = LeftNaturalOrder.infimum isSemilattice } ∧-isOrderTheoreticJoinSemilattice : B.IsJoinSemilattice _≈_ _≥_ _∧_ ∧-isOrderTheoreticJoinSemilattice = record { isPartialOrder = ≥-isPartialOrder ; supremum = B.IsMeetSemilattice.infimum ∧-isOrderTheoreticMeetSemilattice } ∧-orderTheoreticMeetSemilattice : B.MeetSemilattice c ℓ ℓ ∧-orderTheoreticMeetSemilattice = record { isMeetSemilattice = ∧-isOrderTheoreticMeetSemilattice } ∧-orderTheoreticJoinSemilattice : B.JoinSemilattice c ℓ ℓ ∧-orderTheoreticJoinSemilattice = record { isJoinSemilattice = ∧-isOrderTheoreticJoinSemilattice }