------------------------------------------------------------------------
-- The Agda standard library
--
-- Some derivable properties of semilattices
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
open import Algebra.Lattice.Bundles using (Semilattice)
open import Relation.Binary.Bundles using (Poset)
import Relation.Binary.Lattice as B
import Relation.Binary.Properties.Poset as PosetProperties
 
module Algebra.Lattice.Properties.Semilattice
  {c ℓ} (L : Semilattice c ℓ) where
 
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
  }