------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties satisfied by meet semilattices
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

open import Relation.Binary.Lattice

module Relation.Binary.Lattice.Properties.MeetSemilattice
  {c ℓ₁ ℓ₂} (M : MeetSemilattice c ℓ₁ ℓ₂) where

open MeetSemilattice M

open import Algebra.Definitions _≈_
open import Function.Base using (flip)
open import Relation.Binary.Structures using (IsDecPartialOrder)
open import Relation.Binary.Definitions using (Decidable)
open import Relation.Binary.Properties.Poset poset
import Relation.Binary.Lattice.Properties.JoinSemilattice as J

-- The dual construction is a join semilattice.

dualIsJoinSemilattice : IsJoinSemilattice _≈_ (flip _≤_) _∧_
dualIsJoinSemilattice = record
  { isPartialOrder = ≥-isPartialOrder
  ; supremum       = infimum
  }

dualJoinSemilattice : JoinSemilattice c ℓ₁ ℓ₂
dualJoinSemilattice = record
  { _∨_               = _∧_
  ; isJoinSemilattice = dualIsJoinSemilattice
  }

open J dualJoinSemilattice public
  using (isAlgSemilattice; algSemilattice)
  renaming
    ( ∨-monotonic  to ∧-monotonic
    ; ∨-cong       to ∧-cong
    ; ∨-comm       to ∧-comm
    ; ∨-assoc      to ∧-assoc
    ; ∨-idempotent to ∧-idempotent
    ; x≤y⇒x∨y≈y    to y≤x⇒x∧y≈y
    ; ≈-dec⇒≤-dec  to ≈-dec⇒≥-dec
    )

-- If ≈ is decidable then so is ≤

≈-dec⇒≤-dec : Decidable _≈_ → Decidable _≤_
≈-dec⇒≤-dec _≟_ = flip (≈-dec⇒≥-dec _≟_)

≈-dec⇒isDecPartialOrder : Decidable _≈_ → IsDecPartialOrder _≈_ _≤_
≈-dec⇒isDecPartialOrder _≟_ = record
  { isPartialOrder = isPartialOrder
  ; _≟_            = _≟_
  ; _≤?_           = ≈-dec⇒≤-dec _≟_
  }