diff --git a/Lattice.agda b/Lattice.agda
index 139b90e..18ef662 100644
--- a/Lattice.agda
+++ b/Lattice.agda
@@ -16,14 +16,6 @@ record IsSemilattice {a} (A : Set a) (_⊔_ : A → A → A) : Set a where
         ⊔-comm : (x y : A) → x ⊔ y ≡ y ⊔ x
         ⊔-idemp : (x : A) → x ⊔ x ≡ x
 
-record Semilattice {a} (A : Set a) : Set (lsuc a) where
-    field
-        _⊔_ : A → A → A
-
-        isSemilattice : IsSemilattice A _⊔_
-
-    open IsSemilattice isSemilattice public
-
 record IsLattice {a} (A : Set a) (_⊔_ : A → A → A) (_⊓_ : A → A → A) : Set a where
     field
         joinSemilattice : IsSemilattice A _⊔_
@@ -39,6 +31,14 @@ record IsLattice {a} (A : Set a) (_⊔_ : A → A → A) (_⊓_ : A → A → A)
         ; ⊔-idemp to ⊓-idemp
         )
 
+record Semilattice {a} (A : Set a) : Set (lsuc a) where
+    field
+        _⊔_ : A → A → A
+
+        isSemilattice : IsSemilattice A _⊔_
+
+    open IsSemilattice isSemilattice public
+
 
 record Lattice {a} (A : Set a) : Set (lsuc a) where
     field
@@ -49,74 +49,67 @@ record Lattice {a} (A : Set a) : Set (lsuc a) where
 
     open IsLattice isLattice public
 
-module SemilatticeInstances where
+module IsSemilatticeInstances where
     module ForNat where
         open Nat
         open NatProps
         open Eq
 
-        NatMaxSemilattice : Semilattice ℕ
-        NatMaxSemilattice = record
-            { _⊔_ = _⊔_
-            ; isSemilattice = record
-                { ⊔-assoc = ⊔-assoc
-                ; ⊔-comm = ⊔-comm
-                ; ⊔-idemp = ⊔-idem
-                }
+        NatIsMaxSemilattice : IsSemilattice ℕ _⊔_
+        NatIsMaxSemilattice = record
+            { ⊔-assoc = ⊔-assoc
+            ; ⊔-comm = ⊔-comm
+            ; ⊔-idemp = ⊔-idem
             }
 
-        NatMinSemilattice : Semilattice ℕ
-        NatMinSemilattice = record
-            { _⊔_ = _⊓_
-            ; isSemilattice = record
-                { ⊔-assoc = ⊓-assoc
-                ; ⊔-comm = ⊓-comm
-                ; ⊔-idemp = ⊓-idem
-                }
+        NatIsMinSemilattice : IsSemilattice ℕ _⊓_
+        NatIsMinSemilattice = record
+            { ⊔-assoc = ⊓-assoc
+            ; ⊔-comm = ⊓-comm
+            ; ⊔-idemp = ⊓-idem
             }
 
-    module ForProd {a} {A B : Set a} (sA : Semilattice A) (sB : Semilattice B) where
+    module ForProd {a} {A B : Set a}
+        (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B)
+        (sA : IsSemilattice A _⊔₁_) (sB : IsSemilattice B _⊔₂_) where
+
         open Eq
         open Data.Product
 
         private
             _⊔_ : A × B → A × B → A × B
-            (a₁ , b₁) ⊔ (a₂ , b₂) = (Semilattice._⊔_ sA a₁ a₂ , Semilattice._⊔_ sB b₁ 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 Semilattice.⊔-assoc sA a₁ a₂ a₃
-                rewrite Semilattice.⊔-assoc sB b₁ b₂ b₃ = refl
+                rewrite IsSemilattice.⊔-assoc sA a₁ a₂ a₃
+                rewrite IsSemilattice.⊔-assoc sB b₁ b₂ b₃ = refl
 
             ⊔-comm : (p₁ p₂ : A × B) → p₁ ⊔ p₂ ≡ p₂ ⊔ p₁
             ⊔-comm (a₁ , b₁) (a₂ , b₂)
-                rewrite Semilattice.⊔-comm sA a₁ a₂
-                rewrite Semilattice.⊔-comm sB b₁ b₂ = refl
+                rewrite IsSemilattice.⊔-comm sA a₁ a₂
+                rewrite IsSemilattice.⊔-comm sB b₁ b₂ = refl
 
             ⊔-idemp : (p : A × B) → p ⊔ p ≡ p
             ⊔-idemp (a , b)
-                rewrite Semilattice.⊔-idemp sA a
-                rewrite Semilattice.⊔-idemp sB b = refl
+                rewrite IsSemilattice.⊔-idemp sA a
+                rewrite IsSemilattice.⊔-idemp sB b = refl
 
-        ProdSemilattice : Semilattice (A × B)
-        ProdSemilattice = record
-            { _⊔_ = _⊔_
-            ; isSemilattice = record
-                { ⊔-assoc = ⊔-assoc
-                ; ⊔-comm = ⊔-comm
-                ; ⊔-idemp = ⊔-idemp
-                }
+        ProdIsSemilattice : IsSemilattice (A × B) _⊔_
+        ProdIsSemilattice = record
+            { ⊔-assoc = ⊔-assoc
+            ; ⊔-comm = ⊔-comm
+            ; ⊔-idemp = ⊔-idemp
             }
 
-module LatticeInstances where
+module IsLatticeInstances where
     module ForNat where
         open Nat
         open NatProps
         open Eq
-        open SemilatticeInstances.ForNat
+        open IsSemilatticeInstances.ForNat
         open Data.Product
 
-
         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)
@@ -144,29 +137,28 @@ module LatticeInstances 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
 
-        NatLattice : Lattice ℕ
-        NatLattice = record
-            { _⊔_ = _⊔_
-            ; _⊓_ = _⊓_
-            ; isLattice = record
-                { joinSemilattice = Semilattice.isSemilattice NatMaxSemilattice
-                ; meetSemilattice = Semilattice.isSemilattice NatMinSemilattice
-                ; absorb-⊔-⊓ = λ x y → maxmin-absorb {x} {y}
-                ; absorb-⊓-⊔ = λ x y → minmax-absorb {x} {y}
-                }
+        NatIsLattice : IsLattice ℕ _⊔_ _⊓_
+        NatIsLattice = record
+            { joinSemilattice = NatIsMaxSemilattice
+            ; meetSemilattice = NatIsMinSemilattice
+            ; absorb-⊔-⊓ = λ x y → maxmin-absorb {x} {y}
+            ; absorb-⊓-⊔ = λ x y → minmax-absorb {x} {y}
             }
 
-    module ForProd {a} {A B : Set a} (lA : Lattice A) (lB : Lattice B) where
-        private
-            module ProdJoin = SemilatticeInstances.ForProd
-                record { _⊔_ = Lattice._⊔_ lA; isSemilattice = Lattice.joinSemilattice lA }
-                record { _⊔_ = Lattice._⊔_ lB; isSemilattice = Lattice.joinSemilattice lB }
-            module ProdMeet = SemilatticeInstances.ForProd
-                record { _⊔_ = Lattice._⊓_ lA; isSemilattice = Lattice.meetSemilattice lA }
-                record { _⊔_ = Lattice._⊓_ lB; isSemilattice = Lattice.meetSemilattice lB }
+    module ForProd {a} {A B : Set a}
+        (_⊔₁_ : A → A → A) (_⊓₁_ : A → A → A)
+        (_⊔₂_ : B → B → B) (_⊓₂_ : B → B → B)
+        (lA : IsLattice A _⊔₁_ _⊓₁_) (lB : IsLattice B _⊔₂_ _⊓₂_) where
 
-            _⊔_ = Semilattice._⊔_ ProdJoin.ProdSemilattice
-            _⊓_ = Semilattice._⊔_ ProdMeet.ProdSemilattice
+        private
+            module ProdJoin = IsSemilatticeInstances.ForProd _⊔₁_ _⊔₂_ (IsLattice.joinSemilattice lA) (IsLattice.joinSemilattice lB)
+            module ProdMeet = IsSemilatticeInstances.ForProd _⊓₁_ _⊓₂_ (IsLattice.meetSemilattice lA) (IsLattice.meetSemilattice lB)
+
+            _⊔_ : (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
@@ -174,22 +166,18 @@ module LatticeInstances where
         private
             absorb-⊔-⊓ : (p₁ p₂ : A × B) → p₁ ⊔ (p₁ ⊓ p₂) ≡ p₁
             absorb-⊔-⊓ (a₁ , b₁) (a₂ , b₂)
-                rewrite Lattice.absorb-⊔-⊓ lA a₁ a₂
-                rewrite Lattice.absorb-⊔-⊓ lB b₁ b₂ = refl
+                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₂)
-                rewrite Lattice.absorb-⊓-⊔ lA a₁ a₂
-                rewrite Lattice.absorb-⊓-⊔ lB b₁ b₂ = refl
+                rewrite IsLattice.absorb-⊓-⊔ lA a₁ a₂
+                rewrite IsLattice.absorb-⊓-⊔ lB b₁ b₂ = refl
 
-        ProdLattice : Lattice (A × B)
-        ProdLattice = record
-            { _⊔_ = _⊔_
-            ; _⊓_ = _⊓_
-            ; isLattice = record
-                { joinSemilattice = Semilattice.isSemilattice ProdJoin.ProdSemilattice
-                ; meetSemilattice = Semilattice.isSemilattice ProdMeet.ProdSemilattice
-                ; absorb-⊔-⊓ = absorb-⊔-⊓
-                ; absorb-⊓-⊔ = absorb-⊓-⊔
-                }
+        ProdIsLattice : IsLattice (A × B) _⊔_ _⊓_
+        ProdIsLattice = record
+            { joinSemilattice = ProdJoin.ProdIsSemilattice
+            ; meetSemilattice = ProdMeet.ProdIsSemilattice
+            ; absorb-⊔-⊓ = absorb-⊔-⊓
+            ; absorb-⊓-⊔ = absorb-⊓-⊔
             }