diff --git a/Lattice/FiniteMap.agda b/Lattice/FiniteMap.agda
index f4daf57..cfd75ca 100644
--- a/Lattice/FiniteMap.agda
+++ b/Lattice/FiniteMap.agda
@@ -7,11 +7,11 @@ open import Data.List using (List; _∷_; [])
 module Lattice.FiniteMap {A : Set} {B : Set}
     {_≈₂_ : B → B → Set}
     {_⊔₂_ : B → B → B} {_⊓₂_ : B → B → B}
-    (≡-dec-A : IsDecidable (_≡_ {_} {A}))
+    (≡-Decidable-A : IsDecidable {_} {A} _≡_)
     (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
 
 open IsLattice lB using () renaming (_≼_ to _≼₂_)
-open import Lattice.Map ≡-dec-A lB as Map
+open import Lattice.Map ≡-Decidable-A lB as Map
     using
         ( Map
         ; ⊔-equal-keys
diff --git a/Lattice/Map.agda b/Lattice/Map.agda
index b6e49bf..0dbc4a6 100644
--- a/Lattice/Map.agda
+++ b/Lattice/Map.agda
@@ -22,7 +22,7 @@ open import Utils using (Unique; push; Unique-append; All¬-¬Any; All-x∈xs)
 open import Data.String using () renaming (_++_ to _++ˢ_)
 open import Showable using (Showable; show)
 
-open IsDecidable ≡-Decidable-A using () renaming (R-dec to ≡-dec-A)
+open IsDecidable ≡-Decidable-A using () renaming (R-dec to _≟ᴬ_)
 
 open IsLattice lB using () renaming
     ( ≈-refl to ≈₂-refl; ≈-sym to ≈₂-sym; ≈-trans to ≈₂-trans
@@ -42,7 +42,7 @@ private module ImplKeys where
 ∈k-dec : ∀ (k : A) (l : List (A × B)) → Dec (k ∈ˡ (ImplKeys.keys l))
 ∈k-dec k [] = no (λ ())
 ∈k-dec k ((k' , v) ∷ xs)
-    with (≡-dec-A k k')
+    with (k ≟ᴬ k')
 ...   | yes k≡k' = yes (here k≡k')
 ...   | no k≢k' with (∈k-dec k xs)
 ...       | yes k∈kxs = yes (there k∈kxs)
@@ -77,7 +77,7 @@ private module _ where
     k∈-dec : ∀ (k : A) (l : List A) → Dec (k ∈ l)
     k∈-dec k [] = no (λ ())
     k∈-dec k (x ∷ xs)
-        with (≡-dec-A k x)
+        with (k ≟ᴬ x)
     ...   | yes refl = yes (here refl)
     ...   | no k≢x with (k∈-dec k xs)
     ...       | yes k∈xs = yes (there k∈xs)
@@ -114,7 +114,7 @@ private module ImplInsert (f : B → B → B) where
 
     insert : A → B → List (A × B) → List (A × B)
     insert k v [] = (k , v) ∷ []
-    insert k v (x@(k' , v') ∷ xs) with ≡-dec-A k k'
+    insert k v (x@(k' , v') ∷ xs) with k ≟ᴬ k'
     ...                             | yes _ = (k' , f v v') ∷ xs
     ...                             | no _ = x ∷ insert k v xs
 
@@ -124,11 +124,11 @@ private module ImplInsert (f : B → B → B) where
     insert-keys-∈ : ∀ {k : A} {v : B} {l : List (A × B)} →
                     k ∈k l → keys l ≡ keys (insert k v l)
     insert-keys-∈ {k} {v} {(k' , v') ∷ xs} (here k≡k')
-        with (≡-dec-A k k')
+        with (k ≟ᴬ k')
     ...   | yes _ = refl
     ...   | no k≢k' = ⊥-elim (k≢k' k≡k')
     insert-keys-∈ {k} {v} {(k' , _) ∷ xs} (there k∈kxs)
-        with (≡-dec-A k k')
+        with (k ≟ᴬ k')
     ...   | yes _ = refl
     ...   | no _ = cong (λ xs' → k' ∷ xs') (insert-keys-∈ k∈kxs)
 
@@ -136,7 +136,7 @@ private module ImplInsert (f : B → B → B) where
                     ¬ (k ∈k l) → (keys l ++ (k ∷ [])) ≡ keys (insert k v l)
     insert-keys-∉ {k} {v} {[]} _ = refl
     insert-keys-∉ {k} {v} {(k' , v') ∷ xs} k∉kl
-        with (≡-dec-A k k')
+        with (k ≟ᴬ k')
     ...   | yes k≡k' = ⊥-elim (k∉kl (here k≡k'))
     ...   | no _ = cong (λ xs' → k' ∷ xs')
                         (insert-keys-∉ (λ k∈kxs → k∉kl (there k∈kxs)))
@@ -172,7 +172,7 @@ private module ImplInsert (f : B → B → B) where
                                  ¬ k ∈k l → (k , v) ∈ insert k v l
     insert-fresh {l = []} k∉kl = here refl
     insert-fresh {k} {l = (k' , v') ∷ xs} k∉kl
-        with ≡-dec-A k k'
+        with k ≟ᴬ k'
     ...   | yes k≡k' = ⊥-elim (k∉kl (here k≡k'))
     ...   | no _ = there (insert-fresh (λ k∈kxs → k∉kl (there k∈kxs)))
 
@@ -181,9 +181,9 @@ private module ImplInsert (f : B → B → B) where
     insert-preserves-∉k {l = []} k≢k' k∉kl (here k≡k') = k≢k' k≡k'
     insert-preserves-∉k {l = []} k≢k' k∉kl (there ())
     insert-preserves-∉k {k} {k'} {v'} {(k'' , v'') ∷ xs} k≢k' k∉kl k∈kil
-        with ≡-dec-A k k''
+        with k ≟ᴬ k''
     ...   | yes k≡k'' = k∉kl (here k≡k'')
-    ...   | no k≢k'' with ≡-dec-A k' k'' | k∈kil
+    ...   | no k≢k'' with k' ≟ᴬ k'' | k∈kil
     ...       | yes k'≡k'' | here k≡k'' = k≢k'' k≡k''
     ...       | yes k'≡k'' | there k∈kxs = k∉kl (there k∈kxs)
     ...       | no k'≢k''  | here k≡k'' = k∉kl (here k≡k'')
@@ -194,18 +194,18 @@ private module ImplInsert (f : B → B → B) where
                         ¬ k ∈k l₁ → ¬ k ∈k l₂ → ¬ k ∈k union l₁ l₂
     union-preserves-∉ {l₁ = []} _ k∉kl₂ = k∉kl₂
     union-preserves-∉ {k} {(k' , v') ∷ xs₁} k∉kl₁ k∉kl₂
-        with ≡-dec-A k k'
+        with k ≟ᴬ k'
     ...   | yes k≡k' = ⊥-elim (k∉kl₁ (here k≡k'))
     ...   | no k≢k' = insert-preserves-∉k k≢k' (union-preserves-∉ (λ k∈kxs₁ → k∉kl₁ (there k∈kxs₁)) k∉kl₂)
 
     insert-preserves-∈k : ∀ {k k' : A} {v' : B} {l : List (A × B)} →
                           k ∈k l → k ∈k insert k' v' l
     insert-preserves-∈k {k} {k'} {v'} {(k'' , v'') ∷ xs} (here k≡k'')
-        with (≡-dec-A k' k'')
+        with k' ≟ᴬ k''
     ...   | yes _ = here k≡k''
     ...   | no _ = here k≡k''
     insert-preserves-∈k {k} {k'} {v'} {(k'' , v'') ∷ xs} (there k∈kxs)
-        with (≡-dec-A k' k'')
+        with k' ≟ᴬ k''
     ...   | yes _ = there k∈kxs
     ...   | no _ = there (insert-preserves-∈k k∈kxs)
 
@@ -237,11 +237,11 @@ private module ImplInsert (f : B → B → B) where
     insert-preserves-∈ : ∀ {k k' : A} {v v' : B} {l : List (A × B)} →
                          ¬ k ≡ k' → (k , v) ∈ l → (k , v) ∈ insert k' v' l
     insert-preserves-∈ {k} {k'} {l = x ∷ xs} k≢k' (here k,v=x)
-        rewrite sym k,v=x with ≡-dec-A k' k
+        rewrite sym k,v=x with k' ≟ᴬ k
     ...   | yes k'≡k = ⊥-elim (k≢k' (sym k'≡k))
     ...   | no _ = here refl
     insert-preserves-∈ {k} {k'} {l = (k'' , _) ∷ xs} k≢k' (there k,v∈xs)
-        with ≡-dec-A k' k''
+        with k' ≟ᴬ k''
     ...   | yes _ = there k,v∈xs
     ...   | no _ = there (insert-preserves-∈ k≢k' k,v∈xs)
 
@@ -260,7 +260,7 @@ private module ImplInsert (f : B → B → B) where
             k,v∈mxs₁l = union-preserves-∈₁ uxs₁ k,v∈xs₁ k∉kl₂
 
             k≢k' : ¬ k ≡ k'
-            k≢k' with ≡-dec-A k k'
+            k≢k' with k ≟ᴬ k'
             ...    | yes k≡k' rewrite k≡k' = ⊥-elim (All¬-¬Any k'≢xs₁ (∈-cong proj₁ k,v∈xs₁))
             ...    | no  k≢k' = k≢k'
     union-preserves-∈₁ {l₁ = (k' , v') ∷ xs₁} (push k'≢xs₁ uxs₁) (here k,v≡k',v') k∉kl₂
@@ -271,11 +271,11 @@ private module ImplInsert (f : B → B → B) where
                       Unique (keys l) → (k , v') ∈ l → (k , f v v') ∈ (insert k v l)
     insert-combines {l = (k' , v'') ∷ xs} _ (here k,v'≡k',v'')
         rewrite cong proj₁ k,v'≡k',v'' rewrite cong proj₂ k,v'≡k',v''
-        with ≡-dec-A k' k'
+        with k' ≟ᴬ k'
     ...   | yes _ = here refl
     ...   | no k≢k' = ⊥-elim (k≢k' refl)
     insert-combines {k} {l = (k' , v'') ∷ xs} (push k'≢xs uxs) (there k,v'∈xs)
-        with ≡-dec-A k k'
+        with k ≟ᴬ k'
     ...   | yes k≡k' rewrite k≡k' = ⊥-elim (All¬-¬Any k'≢xs (∈-cong proj₁ k,v'∈xs))
     ...   | no k≢k' = there (insert-combines uxs k,v'∈xs)
 
@@ -289,13 +289,13 @@ private module ImplInsert (f : B → B → B) where
         insert-preserves-∈ k≢k' (union-combines uxs₁ ul₂ k,v₁∈xs₁ k,v₂∈l₂)
         where
             k≢k' : ¬ k ≡ k'
-            k≢k' with ≡-dec-A k k'
+            k≢k' with k ≟ᴬ k'
             ...    | yes k≡k' rewrite k≡k' = ⊥-elim (All¬-¬Any k'≢xs₁ (∈-cong proj₁ k,v₁∈xs₁))
             ...    | no  k≢k' = k≢k'
 
     update : A → B → List (A × B) → List (A × B)
     update k v [] = []
-    update k v ((k' , v') ∷ xs) with ≡-dec-A k k'
+    update k v ((k' , v') ∷ xs) with k ≟ᴬ k'
     ...                            | yes _ = (k' , f v v') ∷ xs
     ...                            | no _ = (k' , v') ∷ update k v xs
 
@@ -315,7 +315,7 @@ private module ImplInsert (f : B → B → B) where
                   keys l ≡ keys (update k v l)
     update-keys {l = []} = refl
     update-keys {k} {v} {l = (k' , v') ∷ xs}
-        with ≡-dec-A k k'
+        with k ≟ᴬ k'
     ...   | yes _ = refl
     ...   | no _ rewrite update-keys {k} {v} {xs} = refl
 
@@ -432,11 +432,11 @@ private module ImplInsert (f : B → B → B) where
                          ¬ k ≡ k' → (k , v) ∈ l → (k , v) ∈ update k' v' l
     update-preserves-∈ {k} {k'} {v} {v'} {(k'' , v'') ∷ xs} k≢k' (here k,v≡k'',v'')
         rewrite cong proj₁ k,v≡k'',v'' rewrite cong proj₂ k,v≡k'',v''
-        with ≡-dec-A k' k''
+        with k' ≟ᴬ k''
     ...   | yes k'≡k'' = ⊥-elim (k≢k' (sym k'≡k''))
     ...   | no _ = here refl
     update-preserves-∈ {k} {k'} {v} {v'} {(k'' , v'') ∷ xs} k≢k' (there k,v∈xs)
-        with ≡-dec-A k' k''
+        with k' ≟ᴬ k''
     ...   | yes _ = there k,v∈xs
     ...   | no _ = there (update-preserves-∈ k≢k' k,v∈xs)
 
@@ -450,11 +450,11 @@ private module ImplInsert (f : B → B → B) where
                       Unique (keys l) → (k , v) ∈ l → (k , f v' v) ∈ update k v' l
     update-combines {k} {v} {v'} {(k' , v'') ∷ xs} _ (here k,v=k',v'')
         rewrite cong proj₁ k,v=k',v'' rewrite cong proj₂ k,v=k',v''
-        with ≡-dec-A k' k'
+        with k' ≟ᴬ k'
     ...   | yes _ = here refl
     ...   | no k'≢k' = ⊥-elim (k'≢k' refl)
     update-combines {k} {v} {v'} {(k' , v'') ∷ xs} (push k'≢xs uxs) (there k,v∈xs)
-        with ≡-dec-A k k'
+        with k ≟ᴬ k'
     ...   | yes k≡k' rewrite k≡k' = ⊥-elim (All¬-¬Any k'≢xs (∈-cong proj₁ k,v∈xs))
     ...   | no _ = there (update-combines uxs k,v∈xs)
 
@@ -468,7 +468,7 @@ private module ImplInsert (f : B → B → B) where
         update-preserves-∈ k≢k' (updates-combine uxs₁ u₂ k,v₁∈xs k,v₂∈l₂)
         where
             k≢k' : ¬ k ≡ k'
-            k≢k' with ≡-dec-A k k'
+            k≢k' with k ≟ᴬ k'
             ...    | yes k≡k' rewrite k≡k' = ⊥-elim (All¬-¬Any k'≢xs (∈-cong proj₁ k,v₁∈xs))
             ...    | no  k≢k' = k≢k'