diff --git a/Fixedpoint.agda b/Fixedpoint.agda
index 5fcf2ea..388fcaf 100644
--- a/Fixedpoint.agda
+++ b/Fixedpoint.agda
@@ -5,7 +5,7 @@ module Fixedpoint {a} {A : Set a}
                   {h : ℕ}
                   {_≈_ : A → A → Set a}
                   {_⊔_ : A → A → A} {_⊓_ : A → A → A}
-                  (decA : IsDecidable _≈_)
+                  (≈-dec : IsDecidable _≈_)
                   (flA : IsFiniteHeightLattice A h _≈_ _⊔_ _⊓_)
                   (f : A → A)
                   (Monotonicᶠ : Monotonic (IsFiniteHeightLattice._≼_ flA)
@@ -16,12 +16,11 @@ open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
 open import Relation.Binary.PropositionalEquality using (_≡_; sym)
 open import Relation.Nullary using (Dec; ¬_; yes; no)
 
+open IsFiniteHeightLattice flA
+
 import Chain
 module ChainA = Chain _≈_ ≈-equiv _≺_ ≺-cong
 
-open IsDecidable decA using () renaming (R-dec to ≈-dec)
-open IsFiniteHeightLattice flA
-
 private
     ⊥ᴬ : A
     ⊥ᴬ = proj₁ (proj₁ (proj₁ fixedHeight))
diff --git a/Lattice.agda b/Lattice.agda
index 600da6d..b49afd8 100644
--- a/Lattice.agda
+++ b/Lattice.agda
@@ -19,9 +19,8 @@ open import Data.Empty using (⊥)
 absurd : ∀ {a} {A : Set a} →  ⊥ → A
 absurd ()
 
-record IsDecidable {a} {A : Set a} (R : A → A → Set a) : Set a where
-    field
-        R-dec : ∀ (a₁ a₂ : A) → Dec (R a₁ a₂)
+IsDecidable : ∀ {a} {A : Set a} (R : A → A → Set a) → Set a
+IsDecidable {a} {A} R = ∀ (a₁ a₂ : A) → Dec (R a₁ a₂)
 
 record IsSemilattice {a} (A : Set a)
     (_≈_ : A → A → Set a)
@@ -361,7 +360,7 @@ module IsLatticeInstances where
 module IsFiniteHeightLatticeInstances where
     module ForProd {a} {A B : Set a}
         (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a)
-        (decA : IsDecidable _≈₁_) (decB : IsDecidable _≈₂_)
+        (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
         (_⊔₁_ : A → A → A) (_⊓₁_ : A → A → A)
         (_⊔₂_ : B → B → B) (_⊓₂_ : B → B → B)
         (h₁ h₂ : ℕ)
@@ -373,8 +372,6 @@ module IsFiniteHeightLatticeInstances where
         open IsLattice ProdLattice.ProdIsLattice using (_≼_; _≺_; ≺-cong; ≈-equiv)
         open IsFiniteHeightLattice lA using () renaming (⊔-idemp to ⊔₁-idemp; _≼_ to _≼₁_; ≈-equiv to ≈₁-equiv; ≈-refl to ≈₁-refl; ≈-trans to ≈₁-trans; ≈-sym to ≈₁-sym; _≺_ to _≺₁_; ≺-cong to ≺₁-cong)
         open IsFiniteHeightLattice lB using () renaming (⊔-idemp to ⊔₂-idemp; _≼_ to _≼₂_; ≈-equiv to ≈₂-equiv; ≈-refl to ≈₂-refl; ≈-trans to ≈₂-trans; ≈-sym to ≈₂-sym; _≺_ to _≺₂_; ≺-cong to ≺₂-cong)
-        open IsDecidable decA using () renaming (R-dec to ≈₁-dec)
-        open IsDecidable decB using () renaming (R-dec to ≈₂-dec)
 
         module ChainMapping₁ = ChainMapping (IsFiniteHeightLattice.joinSemilattice lA) (IsLattice.joinSemilattice ProdLattice.ProdIsLattice)
         module ChainMapping₂ = ChainMapping (IsFiniteHeightLattice.joinSemilattice lB) (IsLattice.joinSemilattice ProdLattice.ProdIsLattice)