------------------------------------------------------------------------
-- 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 import Function.Base using (flip)
open import Relation.Binary.Structures using (IsDecPartialOrder)
open import Relation.Binary.Definitions using (Decidable)
open MeetSemilattice M
open import Relation.Binary.Properties.Poset poset using (≥-isPartialOrder)
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 _≟_
}
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4