------------------------------------------------------------------------
-- The Agda standard library
--
-- Some derivable properties of semilattices
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Algebra.Lattice.Bundles using (Semilattice)
module Algebra.Lattice.Properties.Semilattice
{c ℓ} (L : Semilattice c ℓ) where
open import Relation.Binary.Bundles using (Poset)
import Relation.Binary.Lattice as B
import Relation.Binary.Properties.Poset as PosetProperties
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
}
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