diff --git a/Lattice.agda b/Lattice.agda
index 3194c1d..caa714c 100644
--- a/Lattice.agda
+++ b/Lattice.agda
@@ -90,33 +90,33 @@ module IsEquivalenceInstances where
             _⊆_ : Map → Map → Set (Agda.Primitive._⊔_ a b)
             _⊆_ = subset _≈₂_
 
-            ⊆-refl : {m : Map} →  m ⊆ m
-            ⊆-refl k v k,v∈m = (v , (≈₂-refl , k,v∈m))
+            ⊆-refl : (m : Map) →  m ⊆ m
+            ⊆-refl _ k v k,v∈m = (v , (≈₂-refl , k,v∈m))
 
-            ⊆-trans : {m₁ m₂ m₃ : Map} →  m₁ ⊆ m₂ → m₂ ⊆ m₃ → m₁ ⊆ m₃
-            ⊆-trans m₁⊆m₂ m₂⊆m₃ k v k,v∈m₁ =
+            ⊆-trans : (m₁ m₂ m₃ : Map) →  m₁ ⊆ m₂ → m₂ ⊆ m₃ → m₁ ⊆ m₃
+            ⊆-trans _ _ _ m₁⊆m₂ m₂⊆m₃ k v k,v∈m₁ =
                 let
                     (v' , (v≈v' , k,v'∈m₂)) = m₁⊆m₂ k v k,v∈m₁
                     (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})
+            ≈-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₂)
+            ≈-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₂) =
-                ( ⊆-trans {m₁} {m₂} {m₃} m₁⊆m₂ m₂⊆m₃
-                , ⊆-trans {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₂) =
+                ( ⊆-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₃}
+                { ≈-refl = λ {m₁} → ≈-refl m₁
+                ; ≈-sym = λ {m₁} {m₂} → ≈-sym m₁ m₂
+                ; ≈-trans = λ {m₁} {m₂} {m₃} → ≈-trans m₁ m₂ m₃
                 }
 
 module IsSemilatticeInstances where