From 77e2572157a5d9aa540431981615afe88fcda870 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 30 Jul 2023 21:50:28 -0700 Subject: [PATCH] Tweak the style of the Semilattice instance --- Lattice.agda | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/Lattice.agda b/Lattice.agda index b4097e8..9bb8b71 100644 --- a/Lattice.agda +++ b/Lattice.agda @@ -223,6 +223,10 @@ module IsSemilatticeInstances where (sB : IsSemilattice B _≈₂_ _⊔₂_) where 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 infix 4 _≈_ @@ -239,9 +243,9 @@ module IsSemilatticeInstances where MapIsUnionSemilattice : IsSemilattice Map _≈_ _⊔_ MapIsUnionSemilattice = record { ≈-equiv = MapEquiv.LiftEquivalence - ; ⊔-assoc = union-assoc _≈₂_ (IsSemilattice.≈-refl sB) (IsSemilattice.≈-sym sB) _⊔₂_ (IsSemilattice.⊔-assoc sB) - ; ⊔-comm = union-comm _≈₂_ (IsSemilattice.≈-refl sB) (IsSemilattice.≈-sym sB) _⊔₂_ (IsSemilattice.⊔-comm sB) - ; ⊔-idemp = union-idemp _≈₂_ (IsSemilattice.≈-refl sB) (IsSemilattice.≈-sym sB) _⊔₂_ (IsSemilattice.⊔-idemp sB) + ; ⊔-assoc = union-assoc _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-assoc + ; ⊔-comm = union-comm _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-comm + ; ⊔-idemp = union-idemp _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-idemp } module IsLatticeInstances where