------------------------------------------------------------------------
-- The Agda standard library
--
-- Some derivable properties of semilattices
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

open import Algebra.Lattice
open import Algebra.Structures
open import Function
open import Data.Product
open import Relation.Binary
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
  }