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

Tweak the style of the Semilattice instance

Browse Source
This commit is contained in:
Danila Fedorin 2023-07-30 21:50:28 -07:00
parent 1b7a3f02eb
commit 77e2572157
1 changed files with 7 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
Lattice.agda
View File

@ -223,6 +223,10 @@ module IsSemilatticeInstances where
(sB : IsSemilattice B _≈₂_ _⊔₂_) where (sB : IsSemilattice B _≈₂_ _⊔₂_) where
open import Map A B ≡-dec-A open import Map A B ≡-dec-A
open IsSemilattice sB renaming
( ≈-refl to ≈₂-refl; ≈-sym to ≈₂-sym
; ⊔-assoc to ⊔₂-assoc; ⊔-comm to ⊔₂-comm; ⊔-idemp to ⊔₂-idemp
)
private private
infix 4 _≈_ infix 4 _≈_
@ -239,9 +243,9 @@ module IsSemilatticeInstances where
MapIsUnionSemilattice : IsSemilattice Map _≈_ _⊔_ MapIsUnionSemilattice : IsSemilattice Map _≈_ _⊔_
MapIsUnionSemilattice = record MapIsUnionSemilattice = record
{ ≈-equiv = MapEquiv.LiftEquivalence { ≈-equiv = MapEquiv.LiftEquivalence
; ⊔-assoc = union-assoc _≈₂_ (IsSemilattice.≈-refl sB) (IsSemilattice.≈-sym sB) _⊔₂_ (IsSemilattice.⊔-assoc sB) ; ⊔-assoc = union-assoc _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-assoc
; ⊔-comm = union-comm _≈₂_ (IsSemilattice.≈-refl sB) (IsSemilattice.≈-sym sB) _⊔₂_ (IsSemilattice.⊔-comm sB) ; ⊔-comm = union-comm _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-comm
; ⊔-idemp = union-idemp _≈₂_ (IsSemilattice.≈-refl sB) (IsSemilattice.≈-sym sB) _⊔₂_ (IsSemilattice.⊔-idemp sB) ; ⊔-idemp = union-idemp _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-idemp
} }
module IsLatticeInstances where module IsLatticeInstances where