{-# 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
poset : Poset c ℓ ℓ
poset = LeftNaturalOrder.poset isSemilattice
open Poset poset using (_≤_; isPartialOrder)
open PosetProperties poset using (_≥_; ≥-isPartialOrder)
∧-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
}