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