diff --git a/Lattice.agda b/Lattice.agda
index 18ef662..1873547 100644
--- a/Lattice.agda
+++ b/Lattice.agda
@@ -10,19 +10,26 @@ open import Agda.Primitive using (lsuc; Level)
 
 open import NatMap using (NatMap)
 
-record IsSemilattice {a} (A : Set a) (_⊔_ : A → A → A) : Set a where
-    field
-        ⊔-assoc : (x y z : A) → (x ⊔ y) ⊔ z ≡ x ⊔ (y ⊔ z)
-        ⊔-comm : (x y : A) → x ⊔ y ≡ y ⊔ x
-        ⊔-idemp : (x : A) → x ⊔ x ≡ x
+record IsSemilattice {a} (A : Set a)
+    (_≈_ : A → A → Set a)
+    (_⊔_ : A → A → A) : Set a where
 
-record IsLattice {a} (A : Set a) (_⊔_ : A → A → A) (_⊓_ : A → A → A) : Set a where
     field
-        joinSemilattice : IsSemilattice A _⊔_
-        meetSemilattice : IsSemilattice A _⊓_
+        ⊔-assoc : (x y z : A) → ((x ⊔ y) ⊔ z) ≈ (x ⊔ (y ⊔ z))
+        ⊔-comm : (x y : A) → (x ⊔ y) ≈ (y ⊔ x)
+        ⊔-idemp : (x : A) → (x ⊔ x) ≈ x
 
-        absorb-⊔-⊓ : (x y : A) → x ⊔ (x ⊓ y) ≡ x
-        absorb-⊓-⊔ : (x y : A) → x ⊓ (x ⊔ y) ≡ x
+record IsLattice {a} (A : Set a)
+    (_≈_ : A → A → Set a)
+    (_⊔_ : A → A → A)
+    (_⊓_ : A → A → A) : Set a where
+
+    field
+        joinSemilattice : IsSemilattice A _≈_ _⊔_
+        meetSemilattice : IsSemilattice A _≈_ _⊓_
+
+        absorb-⊔-⊓ : (x y : A) → (x ⊔ (x ⊓ y)) ≈ x
+        absorb-⊓-⊔ : (x y : A) → (x ⊓ (x ⊔ y)) ≈ x
 
     open IsSemilattice joinSemilattice public
     open IsSemilattice meetSemilattice public renaming
@@ -33,19 +40,21 @@ record IsLattice {a} (A : Set a) (_⊔_ : A → A → A) (_⊓_ : A → A → A)
 
 record Semilattice {a} (A : Set a) : Set (lsuc a) where
     field
+        _≈_ : A → A → Set a
         _⊔_ : A → A → A
 
-        isSemilattice : IsSemilattice A _⊔_
+        isSemilattice : IsSemilattice A _≈_ _⊔_
 
     open IsSemilattice isSemilattice public
 
 
 record Lattice {a} (A : Set a) : Set (lsuc a) where
     field
+        _≈_ : A → A → Set a
         _⊔_ : A → A → A
         _⊓_ : A → A → A
 
-        isLattice : IsLattice A _⊔_ _⊓_
+        isLattice : IsLattice A _≈_ _⊔_ _⊓_
 
     open IsLattice isLattice public
 
@@ -55,14 +64,14 @@ module IsSemilatticeInstances where
         open NatProps
         open Eq
 
-        NatIsMaxSemilattice : IsSemilattice ℕ _⊔_
+        NatIsMaxSemilattice : IsSemilattice ℕ _≡_ _⊔_
         NatIsMaxSemilattice = record
             { ⊔-assoc = ⊔-assoc
             ; ⊔-comm = ⊔-comm
             ; ⊔-idemp = ⊔-idem
             }
 
-        NatIsMinSemilattice : IsSemilattice ℕ _⊓_
+        NatIsMinSemilattice : IsSemilattice ℕ _≡_ _⊓_
         NatIsMinSemilattice = record
             { ⊔-assoc = ⊓-assoc
             ; ⊔-comm = ⊓-comm
@@ -70,32 +79,42 @@ module IsSemilatticeInstances where
             }
 
     module ForProd {a} {A B : Set a}
+        (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a)
         (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B)
-        (sA : IsSemilattice A _⊔₁_) (sB : IsSemilattice B _⊔₂_) where
+        (sA : IsSemilattice A _≈₁_ _⊔₁_) (sB : IsSemilattice B _≈₂_ _⊔₂_) where
 
         open Eq
         open Data.Product
 
         private
+            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₂)
 
-            ⊔-assoc : (p₁ p₂ p₃ : A × B) → (p₁ ⊔ p₂) ⊔ p₃ ≡ p₁ ⊔ (p₂ ⊔ p₃)
-            ⊔-assoc (a₁ , b₁) (a₂ , b₂) (a₃ , b₃)
-                rewrite IsSemilattice.⊔-assoc sA a₁ a₂ a₃
-                rewrite IsSemilattice.⊔-assoc sB b₁ b₂ b₃ = refl
+            ⊔-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₂)
-                rewrite IsSemilattice.⊔-comm sA a₁ a₂
-                rewrite IsSemilattice.⊔-comm sB b₁ b₂ = refl
+            ⊔-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)
-                rewrite IsSemilattice.⊔-idemp sA a
-                rewrite IsSemilattice.⊔-idemp sB b = refl
+            ⊔-idemp : (p : A × B) → p ⊔ p ≈ p
+            ⊔-idemp (a , b) =
+                ( IsSemilattice.⊔-idemp sA a
+                , IsSemilattice.⊔-idemp sB b
+                )
 
-        ProdIsSemilattice : IsSemilattice (A × B) _⊔_
+        ProdIsSemilattice : IsSemilattice (A × B) _≈_ _⊔_
         ProdIsSemilattice = record
             { ⊔-assoc = ⊔-assoc
             ; ⊔-comm = ⊔-comm
@@ -112,10 +131,13 @@ module IsLatticeInstances where
 
         private
             max-bound₁ : {x y z : ℕ} → x ⊔ y ≡ z → x ≤ z
-            max-bound₁ {x} {y} {z} x⊔y≡z rewrite sym x⊔y≡z rewrite ⊔-comm x y = m≤n⇒m≤o⊔n y (≤-refl)
+            max-bound₁ {x} {y} {z} x⊔y≡z
+                rewrite sym x⊔y≡z
+                rewrite ⊔-comm x y = m≤n⇒m≤o⊔n y (≤-refl)
 
             min-bound₁ : {x y z : ℕ} → x ⊓ y ≡ z → z ≤ x
-            min-bound₁ {x} {y} {z} x⊓y≡z rewrite sym x⊓y≡z = m≤n⇒m⊓o≤n y (≤-refl)
+            min-bound₁ {x} {y} {z} x⊓y≡z
+                rewrite sym x⊓y≡z = m≤n⇒m⊓o≤n y (≤-refl)
 
             minmax-absorb : {x y : ℕ} → x ⊓ (x ⊔ y) ≡ x
             minmax-absorb {x} {y} = ≤-antisym x⊓x⊔y≤x (helper x⊓x≤x⊓x⊔y (⊓-idem x))
@@ -137,7 +159,7 @@ module IsLatticeInstances where
                     helper : x ⊔ (x ⊓ y) ≤ x ⊔ x  → x ⊔ x ≡ x → x ⊔ (x ⊓ y) ≤ x
                     helper x⊔x⊓y≤x⊔x x⊔x≡x rewrite x⊔x≡x = x⊔x⊓y≤x⊔x
 
-        NatIsLattice : IsLattice ℕ _⊔_ _⊓_
+        NatIsLattice : IsLattice ℕ _≡_ _⊔_ _⊓_
         NatIsLattice = record
             { joinSemilattice = NatIsMaxSemilattice
             ; meetSemilattice = NatIsMinSemilattice
@@ -146,13 +168,20 @@ module IsLatticeInstances where
             }
 
     module ForProd {a} {A B : Set a}
+        (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a)
         (_⊔₁_ : A → A → A) (_⊓₁_ : A → A → A)
         (_⊔₂_ : B → B → B) (_⊓₂_ : B → B → B)
-        (lA : IsLattice A _⊔₁_ _⊓₁_) (lB : IsLattice B _⊔₂_ _⊓₂_) where
+        (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)
+            module ProdMeet = IsSemilatticeInstances.ForProd _≈₁_ _≈₂_ _⊓₁_ _⊓₂_ (IsLattice.meetSemilattice lA) (IsLattice.meetSemilattice lB)
+
+            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₂)
@@ -164,17 +193,19 @@ module IsLatticeInstances where
         open Data.Product
 
         private
-            absorb-⊔-⊓ : (p₁ p₂ : A × B) → p₁ ⊔ (p₁ ⊓ p₂) ≡ p₁
-            absorb-⊔-⊓ (a₁ , b₁) (a₂ , b₂)
-                rewrite IsLattice.absorb-⊔-⊓ lA a₁ a₂
-                rewrite IsLattice.absorb-⊔-⊓ lB b₁ b₂ = refl
+            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₂)
-                rewrite IsLattice.absorb-⊓-⊔ lA a₁ a₂
-                rewrite IsLattice.absorb-⊓-⊔ lB b₁ b₂ = refl
+            absorb-⊓-⊔ : (p₁ p₂ : A × B) → p₁ ⊓ (p₁ ⊔ p₂) ≈ p₁
+            absorb-⊓-⊔ (a₁ , b₁) (a₂ , b₂) =
+                ( IsLattice.absorb-⊓-⊔ lA a₁ a₂
+                , IsLattice.absorb-⊓-⊔ lB b₁ b₂
+                )
 
-        ProdIsLattice : IsLattice (A × B) _⊔_ _⊓_
+        ProdIsLattice : IsLattice (A × B) _≈_ _⊔_ _⊓_
         ProdIsLattice = record
             { joinSemilattice = ProdJoin.ProdIsSemilattice
             ; meetSemilattice = ProdMeet.ProdIsSemilattice