------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties satisfied by bounded lattice
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Relation.Binary.Lattice
module Relation.Binary.Lattice.Properties.BoundedLattice
{c ℓ₁ ℓ₂} (L : BoundedLattice c ℓ₁ ℓ₂) where
open import Data.Product.Base using (_,_)
open import Relation.Binary.Bundles using (Setoid)
open BoundedLattice L
open import Algebra.Definitions _≈_ using (Zero; RightZero; LeftZero)
open import Relation.Binary.Lattice.Properties.MeetSemilattice meetSemilattice
using (y≤x⇒x∧y≈y; ∧-comm)
open import Relation.Binary.Lattice.Properties.JoinSemilattice joinSemilattice
using (x≤y⇒x∨y≈y; ∨-comm )
open Setoid setoid renaming (trans to ≈-trans)
∧-zeroʳ : RightZero ⊥ _∧_
∧-zeroʳ x = y≤x⇒x∧y≈y (minimum x)
∧-zeroˡ : LeftZero ⊥ _∧_
∧-zeroˡ x = ≈-trans (∧-comm ⊥ x) (∧-zeroʳ x)
∧-zero : Zero ⊥ _∧_
∧-zero = ∧-zeroˡ , ∧-zeroʳ
∨-zeroʳ : RightZero ⊤ _∨_
∨-zeroʳ x = x≤y⇒x∨y≈y (maximum x)
∨-zeroˡ : LeftZero ⊤ _∨_
∨-zeroˡ x = ≈-trans (∨-comm ⊤ x) (∨-zeroʳ x)
∨-zero : Zero ⊤ _∨_
∨-zero = ∨-zeroˡ , ∨-zeroʳ
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