DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Move < definition to Semilattice

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2023-08-20 19:57:26 -07:00
parent 421f187e8b
commit 561d0f343a
1 changed files with 8 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
Lattice.agda
View File

@ -24,6 +24,12 @@ record IsSemilattice {a} (A : Set a)
(_≈_ : A → A → Set a) (_≈_ : A → A → Set a)
(_⊔_ : A → A → A) : Set a where (_⊔_ : A → A → A) : Set a where
_≼_ : A → A → Set a
a ≼ b = Σ A (λ c → (a ⊔ c) ≈ b)
_≺_ : A → A → Set a
a ≺ b = (a ≼ b) × (¬ a ≈ b)
field field
≈-equiv : IsEquivalence A _≈_ ≈-equiv : IsEquivalence A _≈_
@ -46,7 +52,7 @@ record IsLattice {a} (A : Set a)
absorb-⊓-⊔ : (x y : A) → (x ⊓ (x ⊔ y)) ≈ x absorb-⊓-⊔ : (x y : A) → (x ⊓ (x ⊔ y)) ≈ x
open IsSemilattice joinSemilattice public open IsSemilattice joinSemilattice public
open IsSemilattice meetSemilattice public hiding (≈-equiv; ≈-refl; ≈-sym; ≈-trans) renaming open IsSemilattice meetSemilattice public using () renaming
( ⊔-assoc to ⊓-assoc ( ⊔-assoc to ⊓-assoc
; ⊔-comm to ⊓-comm ; ⊔-comm to ⊓-comm
; ⊔-idemp to ⊓-idemp ; ⊔-idemp to ⊓-idemp
@ -58,15 +64,9 @@ record IsFiniteHeightLattice {a} (A : Set a)
(_⊔_ : A → A → A) (_⊔_ : A → A → A)
(_⊓_ : A → A → A) : Set (lsuc a) where (_⊓_ : A → A → A) : Set (lsuc a) where
_≼_ : A → A → Set a
a ≼ b = Σ A (λ c → (a ⊔ c) ≈ b)
_≺_ : A → A → Set a
a ≺ b = (a ≼ b) × (¬ a ≈ b)
field field
isLattice : IsLattice A _≈_ _⊔_ _⊓_ isLattice : IsLattice A _≈_ _⊔_ _⊓_
fixedHeight : Height _≺_ h fixedHeight : Height (IsLattice._≺_ isLattice) h
open IsLattice isLattice public open IsLattice isLattice public