diff --git a/Lattice.agda b/Lattice.agda
index bdfa791..132ad0f 100644
--- a/Lattice.agda
+++ b/Lattice.agda
@@ -91,6 +91,31 @@ record Lattice {a} (A : Set a) : Set (lsuc a) where
     open IsLattice isLattice public
 
 module IsEquivalenceInstances where
+    module ForProd {a} {A B : Set a}
+        (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a)
+        (eA : IsEquivalence A _≈₁_) (eB : IsEquivalence B _≈₂_) where
+
+        infix 4 _≈_
+
+        _≈_ : A × B → A × B → Set a
+        (a₁ , b₁) ≈ (a₂ , b₂) = (a₁ ≈₁ a₂) × (b₁ ≈₂ b₂)
+
+        ProdEquivalence : IsEquivalence (A × B) _≈_
+        ProdEquivalence = record
+            { ≈-refl = λ {p} →
+                ( IsEquivalence.≈-refl eA
+                , IsEquivalence.≈-refl eB
+                )
+            ; ≈-sym = λ {p₁} {p₂} (a₁≈a₂ , b₁≈b₂) →
+                ( IsEquivalence.≈-sym eA a₁≈a₂
+                , IsEquivalence.≈-sym eB b₁≈b₂
+                )
+            ; ≈-trans = λ {p₁} {p₂} {p₃} (a₁≈a₂ , b₁≈b₂) (a₂≈a₃ , b₂≈b₃) →
+                ( IsEquivalence.≈-trans eA a₁≈a₂ a₂≈a₃
+                , IsEquivalence.≈-trans eB b₁≈b₂ b₂≈b₃
+                )
+            }
+
     module ForMap {a b} (A : Set a) (B : Set b)
         (≡-dec-A : Decidable (_≡_ {a} {A}))
         (_≈₂_ : B → B → Set b)
@@ -105,13 +130,13 @@ module IsEquivalenceInstances where
             ; ≈-trans to ≈₂-trans
             )
 
+        _≈_ : Map → Map → Set (Agda.Primitive._⊔_ a b)
+        _≈_ = lift _≈₂_
+
+        _⊆_ : Map → Map → Set (Agda.Primitive._⊔_ a b)
+        _⊆_ = subset _≈₂_
+
         private
-            _≈_ : Map → Map → Set (Agda.Primitive._⊔_ a b)
-            _≈_ = lift _≈₂_
-
-            _⊆_ : Map → Map → Set (Agda.Primitive._⊔_ a b)
-            _⊆_ = subset _≈₂_
-
             ⊆-refl : (m : Map) →  m ⊆ m
             ⊆-refl _ k v k,v∈m = (v , (≈₂-refl , k,v∈m))
 
@@ -122,23 +147,14 @@ module IsEquivalenceInstances where
                     (v'' , (v'≈v'' , k,v''∈m₃)) = m₂⊆m₃ k v' k,v'∈m₂
                 in (v'' , (≈₂-trans v≈v' v'≈v'' , k,v''∈m₃))
 
-            ≈-refl : (m : Map) → m ≈ m
-            ≈-refl m = (⊆-refl m , ⊆-refl m)
-
-            ≈-sym : (m₁ m₂ : Map) → m₁ ≈ m₂ → m₂ ≈ m₁
-            ≈-sym _ _ (m₁⊆m₂ , m₂⊆m₁) = (m₂⊆m₁ , m₁⊆m₂)
-
-            ≈-trans : (m₁ m₂ m₃ : Map) → m₁ ≈ m₂ → m₂ ≈ m₃ → m₁ ≈ m₃
-            ≈-trans m₁ m₂ m₃ (m₁⊆m₂ , m₂⊆m₁) (m₂⊆m₃ , m₃⊆m₂) =
+        LiftEquivalence : IsEquivalence Map _≈_
+        LiftEquivalence = record
+            { ≈-refl = λ {m} → (⊆-refl m , ⊆-refl m)
+            ; ≈-sym = λ {m₁} {m₂} (m₁⊆m₂ , m₂⊆m₁) → (m₂⊆m₁ , m₁⊆m₂)
+            ; ≈-trans = λ {m₁} {m₂} {m₃} (m₁⊆m₂ , m₂⊆m₁) (m₂⊆m₃ , m₃⊆m₂) →
                 ( ⊆-trans m₁ m₂ m₃ m₁⊆m₂ m₂⊆m₃
                 , ⊆-trans m₃ m₂ m₁ m₃⊆m₂ m₂⊆m₁
                 )
-
-        LiftEquivalence : IsEquivalence Map _≈_
-        LiftEquivalence = record
-            { ≈-refl = λ {m₁} → ≈-refl m₁
-            ; ≈-sym = λ {m₁} {m₂} → ≈-sym m₁ m₂
-            ; ≈-trans = λ {m₁} {m₂} {m₃} → ≈-trans m₁ m₂ m₃
             }
 
 module IsSemilatticeInstances where
@@ -179,63 +195,29 @@ module IsSemilatticeInstances where
         open Eq
         open Data.Product
 
-        private
-            infix 4 _≈_
-            infixl 20 _⊔_
+        module ProdEquiv = IsEquivalenceInstances.ForProd _≈₁_ _≈₂_ (IsSemilattice.≈-equiv sA) (IsSemilattice.≈-equiv sB)
+        open ProdEquiv using (_≈_) public
 
-            _≈_ : A × B → A × B → Set a
-            (a₁ , b₁) ≈ (a₂ , b₂) = (a₁ ≈₁ a₂) × (b₁ ≈₂ b₂)
-
-            _⊔_ : A × B → A × B → A × B
-            (a₁ , b₁) ⊔ (a₂ , b₂) = (a₁ ⊔₁ a₂ , b₁ ⊔₂ b₂)
-
-            ⊔-assoc : (p₁ p₂ p₃ : A × B) → (p₁ ⊔ p₂) ⊔ p₃ ≈ p₁ ⊔ (p₂ ⊔ p₃)
-            ⊔-assoc (a₁ , b₁) (a₂ , b₂) (a₃ , b₃) =
-                ( IsSemilattice.⊔-assoc sA a₁ a₂ a₃
-                , IsSemilattice.⊔-assoc sB b₁ b₂ b₃
-                )
-
-            ⊔-comm : (p₁ p₂ : A × B) → p₁ ⊔ p₂ ≈ p₂ ⊔ p₁
-            ⊔-comm (a₁ , b₁) (a₂ , b₂) =
-                ( IsSemilattice.⊔-comm sA a₁ a₂
-                , IsSemilattice.⊔-comm sB b₁ b₂
-                )
-
-            ⊔-idemp : (p : A × B) → p ⊔ p ≈ p
-            ⊔-idemp (a , b) =
-                ( IsSemilattice.⊔-idemp sA a
-                , IsSemilattice.⊔-idemp sB b
-                )
-
-            ≈-refl : {p : A × B} → p ≈ p
-            ≈-refl =
-                ( IsSemilattice.≈-refl sA
-                , IsSemilattice.≈-refl sB
-                )
-
-            ≈-sym : {p₁ p₂ : A × B} → p₁ ≈ p₂ → p₂ ≈ p₁
-            ≈-sym (a₁≈a₂ , b₁≈b₂) =
-                ( IsSemilattice.≈-sym sA a₁≈a₂
-                , IsSemilattice.≈-sym sB b₁≈b₂
-                )
-
-            ≈-trans : {p₁ p₂ p₃ : A × B} → p₁ ≈ p₂ → p₂ ≈ p₃ → p₁ ≈ p₃
-            ≈-trans (a₁≈a₂ , b₁≈b₂) (a₂≈a₃ , b₂≈b₃) =
-                ( IsSemilattice.≈-trans sA a₁≈a₂ a₂≈a₃
-                , IsSemilattice.≈-trans sB b₁≈b₂ b₂≈b₃
-                )
+        infixl 20 _⊔_
 
+        _⊔_ : A × B → A × B → A × B
+        (a₁ , b₁) ⊔ (a₂ , b₂) = (a₁ ⊔₁ a₂ , b₁ ⊔₂ b₂)
 
         ProdIsSemilattice : IsSemilattice (A × B) _≈_ _⊔_
         ProdIsSemilattice = record
-            { ≈-equiv = record
-                { ≈-refl = ≈-refl
-                ; ≈-sym = ≈-sym
-                ; ≈-trans = ≈-trans
-                }
-            ; ⊔-assoc = ⊔-assoc
-            ; ⊔-comm = ⊔-comm
-            ; ⊔-idemp = ⊔-idemp
+            { ≈-equiv = ProdEquiv.ProdEquivalence
+            ; ⊔-assoc = λ (a₁ , b₁) (a₂ , b₂) (a₃ , b₃) →
+                ( IsSemilattice.⊔-assoc sA a₁ a₂ a₃
+                , IsSemilattice.⊔-assoc sB b₁ b₂ b₃
+                )
+            ; ⊔-comm = λ (a₁ , b₁) (a₂ , b₂) →
+                ( IsSemilattice.⊔-comm sA a₁ a₂
+                , IsSemilattice.⊔-comm sB b₁ b₂
+                )
+            ; ⊔-idemp = λ (a , b) →
+                ( IsSemilattice.⊔-idemp sA a
+                , IsSemilattice.⊔-idemp sB b
+                )
             }
 
     module ForMap {a} {A B : Set a}
@@ -250,20 +232,17 @@ module IsSemilatticeInstances where
             ; ⊔-assoc to ⊔₂-assoc; ⊔-comm to ⊔₂-comm; ⊔-idemp to ⊔₂-idemp
             )
 
-        private
-            infix 4 _≈_
-            infixl 20 _⊔_
-
-            _≈_ : Map → Map → Set a
-            _≈_ = lift (_≈₂_)
-
-            _⊔_ : Map → Map → Map
-            m₁ ⊔ m₂ = union _⊔₂_ m₁ m₂
-
-            _⊓_ : Map → Map → Map
-            m₁ ⊓ m₂ = intersect _⊔₂_ m₁ m₂
-
         module MapEquiv = IsEquivalenceInstances.ForMap A B ≡-dec-A _≈₂_ (IsSemilattice.≈-equiv sB)
+        open MapEquiv using (_≈_) public
+
+        infixl 20 _⊔_
+        infixl 20 _⊓_
+
+        _⊔_ : Map → Map → Map
+        m₁ ⊔ m₂ = union _⊔₂_ m₁ m₂
+
+        _⊓_ : Map → Map → Map
+        m₁ ⊓ m₂ = intersect _⊔₂_ m₁ m₂
 
         MapIsUnionSemilattice : IsSemilattice Map _≈_ _⊔_
         MapIsUnionSemilattice = record
@@ -333,44 +312,24 @@ module IsLatticeInstances where
         (_⊔₂_ : B → B → B) (_⊓₂_ : B → B → B)
         (lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
 
-        private
-            module ProdJoin = IsSemilatticeInstances.ForProd _≈₁_ _≈₂_ _⊔₁_ _⊔₂_ (IsLattice.joinSemilattice lA) (IsLattice.joinSemilattice lB)
-            module ProdMeet = IsSemilatticeInstances.ForProd _≈₁_ _≈₂_ _⊓₁_ _⊓₂_ (IsLattice.meetSemilattice lA) (IsLattice.meetSemilattice lB)
+        module ProdJoin = IsSemilatticeInstances.ForProd _≈₁_ _≈₂_ _⊔₁_ _⊔₂_ (IsLattice.joinSemilattice lA) (IsLattice.joinSemilattice lB)
+        open ProdJoin using (_⊔_; _≈_) public
 
-            infix 4 _≈_
-            infixl 20 _⊔_
-
-            _≈_ : (A × B) → (A × B) → Set a
-            (a₁ , b₁) ≈ (a₂ , b₂) = (a₁ ≈₁ a₂) × (b₁ ≈₂ b₂)
-
-            _⊔_ : (A × B) → (A × B) → (A × B)
-            (a₁ , b₁) ⊔ (a₂ , b₂) = (a₁ ⊔₁ a₂ , b₁ ⊔₂ b₂)
-
-            _⊓_ : (A × B) → (A × B) → (A × B)
-            (a₁ , b₁) ⊓ (a₂ , b₂) = (a₁ ⊓₁ a₂ , b₁ ⊓₂ b₂)
-
-        open Eq
-        open Data.Product
-
-        private
-            absorb-⊔-⊓ : (p₁ p₂ : A × B) → p₁ ⊔ (p₁ ⊓ p₂) ≈ p₁
-            absorb-⊔-⊓ (a₁ , b₁) (a₂ , b₂) =
-                ( IsLattice.absorb-⊔-⊓ lA a₁ a₂
-                , IsLattice.absorb-⊔-⊓ lB b₁ b₂
-                )
-
-            absorb-⊓-⊔ : (p₁ p₂ : A × B) → p₁ ⊓ (p₁ ⊔ p₂) ≈ p₁
-            absorb-⊓-⊔ (a₁ , b₁) (a₂ , b₂) =
-                ( IsLattice.absorb-⊓-⊔ lA a₁ a₂
-                , IsLattice.absorb-⊓-⊔ lB b₁ b₂
-                )
+        module ProdMeet = IsSemilatticeInstances.ForProd _≈₁_ _≈₂_ _⊓₁_ _⊓₂_ (IsLattice.meetSemilattice lA) (IsLattice.meetSemilattice lB)
+        open ProdMeet using () renaming (_⊔_ to _⊓_) public
 
         ProdIsLattice : IsLattice (A × B) _≈_ _⊔_ _⊓_
         ProdIsLattice = record
             { joinSemilattice = ProdJoin.ProdIsSemilattice
             ; meetSemilattice = ProdMeet.ProdIsSemilattice
-            ; absorb-⊔-⊓ = absorb-⊔-⊓
-            ; absorb-⊓-⊔ = absorb-⊓-⊔
+            ; absorb-⊔-⊓ = λ (a₁ , b₁) (a₂ , b₂) →
+                ( IsLattice.absorb-⊔-⊓ lA a₁ a₂
+                , IsLattice.absorb-⊔-⊓ lB b₁ b₂
+                )
+            ; absorb-⊓-⊔ = λ (a₁ , b₁) (a₂ , b₂) →
+                ( IsLattice.absorb-⊓-⊔ lA a₁ a₂
+                , IsLattice.absorb-⊓-⊔ lB b₁ b₂
+                )
             }
 
     module ForMap {a} {A B : Set a}
@@ -387,21 +346,11 @@ module IsLatticeInstances where
             ; absorb-⊔-⊓ to absorb-⊔₂-⊓₂; absorb-⊓-⊔ to absorb-⊓₂-⊔₂
             )
 
-        private
-            module MapJoin = IsSemilatticeInstances.ForMap ≡-dec-A _≈₂_ _⊔₂_ (IsLattice.joinSemilattice lB)
-            module MapMeet = IsSemilatticeInstances.ForMap ≡-dec-A _≈₂_ _⊓₂_ (IsLattice.meetSemilattice lB)
+        module MapJoin = IsSemilatticeInstances.ForMap ≡-dec-A _≈₂_ _⊔₂_ (IsLattice.joinSemilattice lB)
+        open MapJoin using (_⊔_; _≈_) public
 
-            infix 4 _≈_
-            infixl 20 _⊔_
-
-            _≈_ : Map → Map → Set a
-            _≈_ = lift (_≈₂_)
-
-            _⊔_ : Map → Map → Map
-            m₁ ⊔ m₂ = union _⊔₂_ m₁ m₂
-
-            _⊓_ : Map → Map → Map
-            m₁ ⊓ m₂ = intersect _⊓₂_ m₁ m₂
+        module MapMeet = IsSemilatticeInstances.ForMap ≡-dec-A _≈₂_ _⊓₂_ (IsLattice.meetSemilattice lB)
+        open MapMeet using (_⊓_) public
 
         MapIsLattice : IsLattice Map _≈_ _⊔_ _⊓_
         MapIsLattice = record