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

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

open import Algebra

module Algebra.Properties.Semilattice {l₁ l₂} (L : Semilattice l₁ l₂) where

open Semilattice L
open import Algebra.Structures
open import Relation.Binary
import Relation.Binary.Construct.NaturalOrder.Left as LeftNaturalOrder
import Relation.Binary.Lattice as R
import Relation.Binary.Properties.Poset as R
open import Relation.Binary.EqReasoning setoid
open import Function
open import Data.Product

------------------------------------------------------------------------
-- Every semilattice can be turned into a poset via the left natural
-- order.

poset : Poset _ _ _
poset = LeftNaturalOrder.poset _≈_ _∧_ isSemilattice

open Poset poset using (_≤_; isPartialOrder)

------------------------------------------------------------------------
-- Every algebraic semilattice can be turned into an order-theoretic one.

isOrderTheoreticMeetSemilattice : R.IsMeetSemilattice _≈_ _≤_ _∧_
isOrderTheoreticMeetSemilattice = record
  { isPartialOrder = isPartialOrder
  ; infimum        = LeftNaturalOrder.infimum _≈_ _∧_ isSemilattice
  }

orderTheoreticMeetSemilattice : R.MeetSemilattice _ _ _
orderTheoreticMeetSemilattice = record
  { isMeetSemilattice = isOrderTheoreticMeetSemilattice }

isOrderTheoreticJoinSemilattice : R.IsJoinSemilattice _≈_ (flip _≤_) _∧_
isOrderTheoreticJoinSemilattice = record
  { isPartialOrder = R.invIsPartialOrder poset
  ; supremum       = R.IsMeetSemilattice.infimum
                       isOrderTheoreticMeetSemilattice
  }

orderTheoreticJoinSemilattice : R.JoinSemilattice _ _ _
orderTheoreticJoinSemilattice = record
  { isJoinSemilattice = isOrderTheoreticJoinSemilattice }