diff --git a/Analysis/Forward.agda b/Analysis/Forward.agda
index 587bbfe..c3a94da 100644
--- a/Analysis/Forward.agda
+++ b/Analysis/Forward.agda
@@ -2,10 +2,10 @@ open import Language hiding (_[_])
 open import Lattice
 
 module Analysis.Forward
-    {L : Set} {h}
+    (L : Set) {h}
     {_≈ˡ_ : L → L → Set} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L}
-    (isFiniteHeightLatticeˡ : IsFiniteHeightLattice L h _≈ˡ_ _⊔ˡ_ _⊓ˡ_)
-    (≈ˡ-dec : IsDecidable _≈ˡ_) where
+    {{isFiniteHeightLatticeˡ : IsFiniteHeightLattice L h _≈ˡ_ _⊔ˡ_ _⊓ˡ_}}
+    {{≈ˡ-dec : IsDecidable _≈ˡ_}} where
 
 open import Data.Empty using (⊥-elim)
 open import Data.String using (String)
@@ -20,8 +20,8 @@ open IsFiniteHeightLattice isFiniteHeightLatticeˡ
     using () renaming (isLattice to isLatticeˡ)
 
 module WithProg (prog : Program) where
-    open import Analysis.Forward.Lattices isFiniteHeightLatticeˡ ≈ˡ-dec prog
-    open import Analysis.Forward.Evaluation isFiniteHeightLatticeˡ ≈ˡ-dec prog
+    open import Analysis.Forward.Lattices L prog hiding (≈ᵛ-Decidable) -- to disambiguate instance resolution
+    open import Analysis.Forward.Evaluation L prog
     open Program prog
 
     private module WithStmtEvaluator {{evaluator : StmtEvaluator}} where
@@ -43,7 +43,7 @@ module WithProg (prog : Program) where
                             (flip (eval s)) (eval-Monoʳ s)
                             vs₁≼vs₂
 
-        open StateVariablesFiniteMap.GeneralizedUpdate isLatticeᵐ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) updateVariablesForState updateVariablesForState-Monoʳ states
+        open StateVariablesFiniteMap.GeneralizedUpdate {{isLatticeᵐ}} (λ x → x) (λ a₁≼a₂ → a₁≼a₂) updateVariablesForState updateVariablesForState-Monoʳ states
             using ()
             renaming
                 ( f' to updateAll
diff --git a/Analysis/Forward/Adapters.agda b/Analysis/Forward/Adapters.agda
index c1a9e60..2da8ec4 100644
--- a/Analysis/Forward/Adapters.agda
+++ b/Analysis/Forward/Adapters.agda
@@ -2,14 +2,14 @@ open import Language hiding (_[_])
 open import Lattice
 
 module Analysis.Forward.Adapters
-    {L : Set} {h}
+    (L : Set) {h}
     {_≈ˡ_ : L → L → Set} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L}
-    (isFiniteHeightLatticeˡ : IsFiniteHeightLattice L h _≈ˡ_ _⊔ˡ_ _⊓ˡ_)
-    (≈ˡ-dec : IsDecidable _≈ˡ_)
+    {{isFiniteHeightLatticeˡ : IsFiniteHeightLattice L h _≈ˡ_ _⊔ˡ_ _⊓ˡ_}}
+    {{≈ˡ-dec : IsDecidable _≈ˡ_}}
     (prog : Program) where
 
-open import Analysis.Forward.Lattices isFiniteHeightLatticeˡ ≈ˡ-dec prog
-open import Analysis.Forward.Evaluation isFiniteHeightLatticeˡ ≈ˡ-dec prog
+open import Analysis.Forward.Lattices L prog
+open import Analysis.Forward.Evaluation L prog
 
 open import Data.Empty using (⊥-elim)
 open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
@@ -41,7 +41,7 @@ module ExprToStmtAdapter {{ exprEvaluator : ExprEvaluator }} where
     -- for an assignment, and update the corresponding key. Use Exercise 4.26's
     -- generalized update to set the single key's value.
     private module _ (k : String) (e : Expr) where
-        open VariableValuesFiniteMap.GeneralizedUpdate isLatticeᵛ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) (λ _ → evalᵉ e) (λ _ {vs₁} {vs₂} vs₁≼vs₂ → evalᵉ-Monoʳ e {vs₁} {vs₂} vs₁≼vs₂) (k ∷ [])
+        open VariableValuesFiniteMap.GeneralizedUpdate {{isLatticeᵛ}} (λ x → x) (λ a₁≼a₂ → a₁≼a₂) (λ _ → evalᵉ e) (λ _ {vs₁} {vs₂} vs₁≼vs₂ → evalᵉ-Monoʳ e {vs₁} {vs₂} vs₁≼vs₂) (k ∷ [])
             using ()
             renaming
                 ( f' to updateVariablesFromExpression
diff --git a/Analysis/Forward/Evaluation.agda b/Analysis/Forward/Evaluation.agda
index acd681a..8e0763a 100644
--- a/Analysis/Forward/Evaluation.agda
+++ b/Analysis/Forward/Evaluation.agda
@@ -2,13 +2,13 @@ open import Language hiding (_[_])
 open import Lattice
 
 module Analysis.Forward.Evaluation
-    {L : Set} {h}
+    (L : Set) {h}
     {_≈ˡ_ : L → L → Set} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L}
-    (isFiniteHeightLatticeˡ : IsFiniteHeightLattice L h _≈ˡ_ _⊔ˡ_ _⊓ˡ_)
-    (≈ˡ-dec : IsDecidable _≈ˡ_)
+    {{isFiniteHeightLatticeˡ : IsFiniteHeightLattice L h _≈ˡ_ _⊔ˡ_ _⊓ˡ_}}
+    {{≈ˡ-dec : IsDecidable _≈ˡ_}}
     (prog : Program) where
 
-open import Analysis.Forward.Lattices isFiniteHeightLatticeˡ ≈ˡ-dec prog
+open import Analysis.Forward.Lattices L prog
 open import Data.Product using (_,_)
 
 open IsFiniteHeightLattice isFiniteHeightLatticeˡ
diff --git a/Analysis/Forward/Lattices.agda b/Analysis/Forward/Lattices.agda
index 33863d8..f365c83 100644
--- a/Analysis/Forward/Lattices.agda
+++ b/Analysis/Forward/Lattices.agda
@@ -2,20 +2,21 @@ open import Language hiding (_[_])
 open import Lattice
 
 module Analysis.Forward.Lattices
-    {L : Set} {h}
+    (L : Set) {h}
     {_≈ˡ_ : L → L → Set} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L}
-    (isFiniteHeightLatticeˡ : IsFiniteHeightLattice L h _≈ˡ_ _⊔ˡ_ _⊓ˡ_)
-    (≈ˡ-Decidable : IsDecidable _≈ˡ_)
+    {{isFiniteHeightLatticeˡ : IsFiniteHeightLattice L h _≈ˡ_ _⊔ˡ_ _⊓ˡ_}}
+    {{≈ˡ-Decidable : IsDecidable _≈ˡ_}}
     (prog : Program) where
 
-open import Data.String using () renaming (_≟_ to _≟ˢ_)
+open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
 open import Data.Product using (proj₁; proj₂; _,_)
+open import Data.Unit using (tt)
 open import Data.Sum using (inj₁; inj₂)
 open import Data.List using (List; _∷_; []; foldr)
 open import Data.List.Membership.Propositional using () renaming (_∈_ to _∈ˡ_)
 open import Data.List.Relation.Unary.Any as Any using ()
 open import Relation.Binary.PropositionalEquality using (_≡_; refl)
-open import Utils using (Pairwise; _⇒_; _∨_)
+open import Utils using (Pairwise; _⇒_; _∨_; it)
 
 open IsFiniteHeightLattice isFiniteHeightLatticeˡ
     using ()
@@ -29,14 +30,15 @@ open Program prog
 import Lattice.FiniteMap
 import Chain
 
-≡-Decidable-String = record { R-dec = _≟ˢ_ }
-≡-Decidable-State = record { R-dec = _≟_ }
+instance
+    ≡-Decidable-String = record { R-dec = _≟ˢ_ }
+    ≡-Decidable-State = record { R-dec = _≟_ }
 
 -- The variable -> abstract value (e.g. sign) map is a finite value-map
 -- with keys strings. Use a bundle to avoid explicitly specifying operators.
 -- It's helpful to export these via 'public' since consumers tend to
 -- use various variable lattice operations.
-module VariableValuesFiniteMap = Lattice.FiniteMap.WithKeys ≡-Decidable-String isLatticeˡ vars
+module VariableValuesFiniteMap = Lattice.FiniteMap.WithKeys String L tt vars
 open VariableValuesFiniteMap
     using ()
     renaming
@@ -45,7 +47,7 @@ open VariableValuesFiniteMap
         ; _≈_ to _≈ᵛ_
         ; _⊔_ to _⊔ᵛ_
         ; _≼_ to _≼ᵛ_
-        ; ≈₂-Decidable⇒≈-Decidable to ≈ˡ-Decidable⇒≈ᵛ-Decidable
+        ; ≈-Decidable to ≈ᵛ-Decidable
         ; _∈_ to _∈ᵛ_
         ; _∈k_ to _∈kᵛ_
         ; _updating_via_ to _updatingᵛ_via_
@@ -63,27 +65,25 @@ open IsLattice isLatticeᵛ
         ; ⊔-idemp to ⊔ᵛ-idemp
         )
     public
-open Lattice.FiniteMap.IterProdIsomorphism ≡-Decidable-String isLatticeˡ
+open Lattice.FiniteMap.IterProdIsomorphism String L _
     using ()
     renaming
         ( Provenance-union to Provenance-unionᵐ
         )
     public
-open Lattice.FiniteMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight ≡-Decidable-String isLatticeˡ vars-Unique ≈ˡ-Decidable _ fixedHeightˡ
+open Lattice.FiniteMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight String L _ vars-Unique
     using ()
     renaming
         ( isFiniteHeightLattice to isFiniteHeightLatticeᵛ
+        ; fixedHeight to fixedHeightᵛ
         ; ⊥-contains-bottoms to ⊥ᵛ-contains-bottoms
         )
     public
 
-≈ᵛ-Decidable = ≈ˡ-Decidable⇒≈ᵛ-Decidable ≈ˡ-Decidable
-joinSemilatticeᵛ = IsFiniteHeightLattice.joinSemilattice isFiniteHeightLatticeᵛ
-fixedHeightᵛ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵛ
 ⊥ᵛ = Chain.Height.⊥ fixedHeightᵛ
 
 -- Finally, the map we care about is (state -> (variables -> value)). Bring that in.
-module StateVariablesFiniteMap = Lattice.FiniteMap.WithKeys ≡-Decidable-State isLatticeᵛ states
+module StateVariablesFiniteMap = Lattice.FiniteMap.WithKeys State VariableValues tt states
 open StateVariablesFiniteMap
     using (_[_]; []-∈; m₁≼m₂⇒m₁[ks]≼m₂[ks]; m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂)
     renaming
@@ -94,11 +94,11 @@ open StateVariablesFiniteMap
         ; _∈k_ to _∈kᵐ_
         ; locate to locateᵐ
         ; _≼_ to _≼ᵐ_
-        ; ≈₂-Decidable⇒≈-Decidable to ≈ᵛ-Decidable⇒≈ᵐ-Decidable
+        ; ≈-Decidable to ≈ᵐ-Decidable
         ; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ
         )
     public
-open Lattice.FiniteMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight ≡-Decidable-State isLatticeᵛ states-Unique ≈ᵛ-Decidable _ fixedHeightᵛ
+open Lattice.FiniteMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight State VariableValues _ states-Unique
     using ()
     renaming
         ( isFiniteHeightLattice to isFiniteHeightLatticeᵐ
@@ -111,9 +111,6 @@ open IsFiniteHeightLattice isFiniteHeightLatticeᵐ
         )
     public
 
-≈ᵐ-Decidable = ≈ᵛ-Decidable⇒≈ᵐ-Decidable ≈ᵛ-Decidable
-fixedHeightᵐ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵐ
-
 -- We now have our (state -> (variables -> value)) map.
 -- Define a couple of helpers to retrieve values from it. Specifically,
 -- since the State type is as specific as possible, it's always possible to
@@ -147,12 +144,12 @@ joinForKey k states = foldr _⊔ᵛ_ ⊥ᵛ (states [ incoming k ])
 
 joinForKey-Mono : ∀ (k : State) → Monotonic _≼ᵐ_ _≼ᵛ_ (joinForKey k)
 joinForKey-Mono k {fm₁} {fm₂} fm₁≼fm₂ =
-    foldr-Mono joinSemilatticeᵛ joinSemilatticeᵛ (fm₁ [ incoming k ]) (fm₂ [ incoming k ]) _⊔ᵛ_ ⊥ᵛ ⊥ᵛ
+    foldr-Mono it it (fm₁ [ incoming k ]) (fm₂ [ incoming k ]) _⊔ᵛ_ ⊥ᵛ ⊥ᵛ
                (m₁≼m₂⇒m₁[ks]≼m₂[ks] fm₁ fm₂ (incoming k) fm₁≼fm₂)
                (⊔ᵛ-idemp ⊥ᵛ) ⊔ᵛ-Monotonicʳ ⊔ᵛ-Monotonicˡ
 
 -- The name f' comes from the formulation of Exercise 4.26.
-open StateVariablesFiniteMap.GeneralizedUpdate isLatticeᵐ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) joinForKey joinForKey-Mono states
+open StateVariablesFiniteMap.GeneralizedUpdate {{isLatticeᵐ}} (λ x → x) (λ a₁≼a₂ → a₁≼a₂) joinForKey joinForKey-Mono states
     using ()
     renaming
         ( f' to joinAll
diff --git a/Analysis/Sign.agda b/Analysis/Sign.agda
index af72306..913a341 100644
--- a/Analysis/Sign.agda
+++ b/Analysis/Sign.agda
@@ -52,7 +52,6 @@ open import Lattice.AboveBelow Sign _≡_ (record { ≈-refl = refl; ≈-sym = s
     using ()
     renaming
         ( AboveBelow to SignLattice
-        ; ≈-Decidable to ≈ᵍ-Decidable
         ; ⊥ to ⊥ᵍ
         ; ⊤ to ⊤ᵍ
         ; [_] to [_]ᵍ
@@ -72,10 +71,7 @@ open AB.Plain 0ˢ using ()
         ; _⊓_ to _⊓ᵍ_
         )
 
-open IsLattice isLatticeᵍ using ()
-    renaming
-        ( ≼-trans to ≼ᵍ-trans
-        )
+open IsLattice isLatticeᵍ using () renaming (≼-trans to ≼ᵍ-trans)
 
 plus : SignLattice → SignLattice → SignLattice
 plus ⊥ᵍ _ = ⊥ᵍ
@@ -175,9 +171,9 @@ instance
 module WithProg (prog : Program) where
     open Program prog
 
-    open import Analysis.Forward.Lattices isFiniteHeightLatticeᵍ ≈ᵍ-Decidable prog
-    open import Analysis.Forward.Evaluation isFiniteHeightLatticeᵍ ≈ᵍ-Decidable prog
-    open import Analysis.Forward.Adapters isFiniteHeightLatticeᵍ ≈ᵍ-Decidable prog
+    open import Analysis.Forward.Lattices SignLattice prog
+    open import Analysis.Forward.Evaluation SignLattice prog
+    open import Analysis.Forward.Adapters SignLattice prog
 
     eval : ∀ (e : Expr) → VariableValues → SignLattice
     eval (e₁ + e₂) vs = plus (eval e₁ vs) (eval e₂ vs)
@@ -233,7 +229,7 @@ module WithProg (prog : Program) where
         SignEval = record { eval = eval; eval-Monoʳ = eval-Monoʳ }
 
     -- For debugging purposes, print out the result.
-    output = show (Analysis.Forward.WithProg.result isFiniteHeightLatticeᵍ ≈ᵍ-Decidable prog)
+    output = show (Analysis.Forward.WithProg.result SignLattice prog)
 
     -- This should have fewer cases -- the same number as the actual 'plus' above.
     -- But agda only simplifies on first argument, apparently, so we are stuck
diff --git a/Isomorphism.agda b/Isomorphism.agda
index cc79eb8..b4f30b6 100644
--- a/Isomorphism.agda
+++ b/Isomorphism.agda
@@ -63,27 +63,29 @@ module TransportFiniteHeight
         portChain₂ (done₂ a₂≈a₁) = done₁ (g-preserves-≈₂ a₂≈a₁)
         portChain₂ (step₂ {b₁} {b₂} (b₁≼b₂ , b₁̷≈b₂) b₂≈b₂' c) = step₁ (≈₁-trans (≈₁-sym (g-⊔-distr b₁ b₂)) (g-preserves-≈₂ b₁≼b₂) , g-preserves-̷≈ b₁̷≈b₂) (g-preserves-≈₂ b₂≈b₂') (portChain₂ c)
 
-    isFiniteHeightLattice : IsFiniteHeightLattice B height _≈₂_ _⊔₂_ _⊓₂_
-    isFiniteHeightLattice =
-        let
-            open Chain.Height (IsFiniteHeightLattice.fixedHeight fhlA)
-                using ()
-                renaming (⊥ to ⊥₁; ⊤ to ⊤₁; bounded to bounded₁; longestChain to c)
-        in record
-            { isLattice = lB
-            ; fixedHeight = record
-                { ⊥ = f ⊥₁
-                ; ⊤ = f ⊤₁
-                ; longestChain = portChain₁ c
-                ; bounded = λ c' → bounded₁ (portChain₂ c')
-                }
+    open Chain.Height (IsFiniteHeightLattice.fixedHeight fhlA)
+        using ()
+        renaming (⊥ to ⊥₁; ⊤ to ⊤₁; bounded to bounded₁; longestChain to c)
+
+    instance
+        fixedHeight = record
+            { ⊥ = f ⊥₁
+            ; ⊤ = f ⊤₁
+            ; longestChain = portChain₁ c
+            ; bounded = λ c' → bounded₁ (portChain₂ c')
             }
 
-    finiteHeightLattice : FiniteHeightLattice B
-    finiteHeightLattice = record
-        { height = height
-        ; _≈_ = _≈₂_
-        ; _⊔_ = _⊔₂_
-        ; _⊓_ = _⊓₂_
-        ; isFiniteHeightLattice = isFiniteHeightLattice
-        }
+        isFiniteHeightLattice : IsFiniteHeightLattice B height _≈₂_ _⊔₂_ _⊓₂_
+        isFiniteHeightLattice = record
+            { isLattice = lB
+            ; fixedHeight = fixedHeight
+            }
+
+        finiteHeightLattice : FiniteHeightLattice B
+        finiteHeightLattice = record
+            { height = height
+            ; _≈_ = _≈₂_
+            ; _⊔_ = _⊔₂_
+            ; _⊓_ = _⊓₂_
+            ; isFiniteHeightLattice = isFiniteHeightLattice
+            }
diff --git a/Language.agda b/Language.agda
index 8e1706b..506b9f1 100644
--- a/Language.agda
+++ b/Language.agda
@@ -22,7 +22,7 @@ open import Relation.Nullary using (¬_)
 
 open import Lattice
 open import Utils using (Unique; push; Unique-map; x∈xs⇒fx∈fxs)
-open import Lattice.MapSet (record { R-dec = _≟ˢ_ }) using ()
+open import Lattice.MapSet String {{record { R-dec = _≟ˢ_ }}} _ using ()
     renaming
         ( MapSet to StringSet
         ; to-List to to-Listˢ
diff --git a/Language/Base.agda b/Language/Base.agda
index 2e7f21b..5fd6eec 100644
--- a/Language/Base.agda
+++ b/Language/Base.agda
@@ -39,7 +39,7 @@ data _∈ᵇ_ : String → BasicStmt → Set where
     in←₁ : ∀ {k : String} {e : Expr} → k ∈ᵇ (k ← e)
     in←₂ : ∀ {k k' : String} {e : Expr} → k ∈ᵉ e → k ∈ᵇ (k' ← e)
 
-open import Lattice.MapSet (record { R-dec = String._≟_ })
+open import Lattice.MapSet String {{record { R-dec = String._≟_ }}} _
     renaming
         ( MapSet to StringSet
         ; insert to insertˢ
diff --git a/Lattice.agda b/Lattice.agda
index 20ecacc..d8a75ce 100644
--- a/Lattice.agda
+++ b/Lattice.agda
@@ -187,8 +187,8 @@ record IsLattice {a} (A : Set a)
     (_⊓_ : A → A → A) : Set a where
 
     field
-        joinSemilattice : IsSemilattice A _≈_ _⊔_
-        meetSemilattice : IsSemilattice A _≈_ _⊓_
+        {{joinSemilattice}} : IsSemilattice A _≈_ _⊔_
+        {{meetSemilattice}} : IsSemilattice A _≈_ _⊓_
 
         absorb-⊔-⊓ : (x y : A) → (x ⊔ (x ⊓ y)) ≈ x
         absorb-⊓-⊔ : (x y : A) → (x ⊓ (x ⊔ y)) ≈ x
@@ -217,12 +217,12 @@ record IsFiniteHeightLattice {a} (A : Set a)
     (_⊓_ : A → A → A) : Set (lsuc a) where
 
     field
-        isLattice : IsLattice A _≈_ _⊔_ _⊓_
+        {{isLattice}} : IsLattice A _≈_ _⊔_ _⊓_
 
     open IsLattice isLattice public
 
     field
-        fixedHeight : FixedHeight h
+        {{fixedHeight}} : FixedHeight h
 
 module ChainMapping {a b} {A : Set a} {B : Set b}
     {_≈₁_ : A → A → Set a} {_≈₂_ : B → B → Set b}
@@ -252,7 +252,7 @@ record Semilattice {a} (A : Set a) : Set (lsuc a) where
         _≈_ : A → A → Set a
         _⊔_ : A → A → A
 
-        isSemilattice : IsSemilattice A _≈_ _⊔_
+        {{isSemilattice}} : IsSemilattice A _≈_ _⊔_
 
     open IsSemilattice isSemilattice public
 
@@ -263,7 +263,7 @@ record Lattice {a} (A : Set a) : Set (lsuc a) where
         _⊔_ : A → A → A
         _⊓_ : A → A → A
 
-        isLattice : IsLattice A _≈_ _⊔_ _⊓_
+        {{isLattice}} : IsLattice A _≈_ _⊔_ _⊓_
 
     open IsLattice isLattice public
 
@@ -274,6 +274,6 @@ record FiniteHeightLattice {a} (A : Set a) : Set (lsuc a) where
         _⊔_ : A → A → A
         _⊓_ : A → A → A
 
-        isFiniteHeightLattice : IsFiniteHeightLattice A height _≈_ _⊔_ _⊓_
+        {{isFiniteHeightLattice}} : IsFiniteHeightLattice A height _≈_ _⊔_ _⊓_
 
     open IsFiniteHeightLattice isFiniteHeightLattice public
diff --git a/Lattice/AboveBelow.agda b/Lattice/AboveBelow.agda
index d2aecdd..2cce13f 100644
--- a/Lattice/AboveBelow.agda
+++ b/Lattice/AboveBelow.agda
@@ -79,8 +79,9 @@ data _≈_ : AboveBelow → AboveBelow → Set a where
 ≈-dec [ x ] ⊥ = no λ ()
 ≈-dec [ x ] ⊤ = no λ ()
 
-≈-Decidable : IsDecidable _≈_
-≈-Decidable = record { R-dec = ≈-dec }
+instance
+    ≈-Decidable : IsDecidable _≈_
+    ≈-Decidable = record { R-dec = ≈-dec }
 
 -- Any object can be wrapped in an 'above below' to make it a lattice,
 -- since ⊤ and ⊥ are the largest and least elements, and the rest are left
@@ -175,14 +176,15 @@ module Plain (x : A) where
     ⊔-idemp ⊥ = ≈-⊥-⊥
     ⊔-idemp [ x ] rewrite x≈y⇒[x]⊔[y]≡[x] (≈₁-refl {x}) = ≈-refl
 
-    isJoinSemilattice : IsSemilattice AboveBelow _≈_ _⊔_
-    isJoinSemilattice = record
-        { ≈-equiv = ≈-equiv
-        ; ≈-⊔-cong = ≈-⊔-cong
-        ; ⊔-assoc = ⊔-assoc
-        ; ⊔-comm = ⊔-comm
-        ; ⊔-idemp = ⊔-idemp
-        }
+    instance
+        isJoinSemilattice : IsSemilattice AboveBelow _≈_ _⊔_
+        isJoinSemilattice = record
+            { ≈-equiv = ≈-equiv
+            ; ≈-⊔-cong = ≈-⊔-cong
+            ; ⊔-assoc = ⊔-assoc
+            ; ⊔-comm = ⊔-comm
+            ; ⊔-idemp = ⊔-idemp
+            }
 
     _⊓_ : AboveBelow → AboveBelow → AboveBelow
     ⊥ ⊓ x = ⊥
@@ -268,14 +270,15 @@ module Plain (x : A) where
     ⊓-idemp ⊤ = ≈-⊤-⊤
     ⊓-idemp [ x ] rewrite x≈y⇒[x]⊓[y]≡[x] (≈₁-refl {x}) = ≈-refl
 
-    isMeetSemilattice : IsSemilattice AboveBelow _≈_ _⊓_
-    isMeetSemilattice = record
-        { ≈-equiv = ≈-equiv
-        ; ≈-⊔-cong = ≈-⊓-cong
-        ; ⊔-assoc = ⊓-assoc
-        ; ⊔-comm = ⊓-comm
-        ; ⊔-idemp = ⊓-idemp
-        }
+    instance
+        isMeetSemilattice : IsSemilattice AboveBelow _≈_ _⊓_
+        isMeetSemilattice = record
+            { ≈-equiv = ≈-equiv
+            ; ≈-⊔-cong = ≈-⊓-cong
+            ; ⊔-assoc = ⊓-assoc
+            ; ⊔-comm = ⊓-comm
+            ; ⊔-idemp = ⊓-idemp
+            }
 
     absorb-⊔-⊓ : ∀ (ab₁ ab₂ : AboveBelow) → (ab₁ ⊔ (ab₁ ⊓ ab₂)) ≈ ab₁
     absorb-⊔-⊓ ⊥ ab₂ rewrite ⊥⊓x≡⊥ ab₂ = ≈-⊥-⊥
@@ -300,21 +303,22 @@ module Plain (x : A) where
     ...   | no x̷≈y rewrite x̷≈y⇒[x]⊔[y]≡⊤ x̷≈y rewrite x⊓⊤≡x [ x ] = ≈-refl
 
 
-    isLattice : IsLattice AboveBelow _≈_ _⊔_ _⊓_
-    isLattice = record
-        { joinSemilattice = isJoinSemilattice
-        ; meetSemilattice = isMeetSemilattice
-        ; absorb-⊔-⊓ = absorb-⊔-⊓
-        ; absorb-⊓-⊔ = absorb-⊓-⊔
-        }
+    instance
+        isLattice : IsLattice AboveBelow _≈_ _⊔_ _⊓_
+        isLattice = record
+            { joinSemilattice = isJoinSemilattice
+            ; meetSemilattice = isMeetSemilattice
+            ; absorb-⊔-⊓ = absorb-⊔-⊓
+            ; absorb-⊓-⊔ = absorb-⊓-⊔
+            }
 
-    lattice : Lattice AboveBelow
-    lattice = record
-        { _≈_ = _≈_
-        ; _⊔_ = _⊔_
-        ; _⊓_ = _⊓_
-        ; isLattice = isLattice
-        }
+        lattice : Lattice AboveBelow
+        lattice = record
+            { _≈_ = _≈_
+            ; _⊔_ = _⊔_
+            ; _⊓_ = _⊓_
+            ; isLattice = isLattice
+            }
 
     open IsLattice isLattice using (_≼_; _≺_; ⊔-Monotonicˡ; ⊔-Monotonicʳ) public
 
@@ -360,25 +364,26 @@ module Plain (x : A) where
     isLongest {⊥} (step {_} {[ x ]} _ (≈-lift _) (step [x]≺y y≈z c@(step _ _ _)))
         rewrite [x]≺y⇒y≡⊤ _ _ [x]≺y with ≈-⊤-⊤ ← y≈z = ⊥-elim (¬-Chain-⊤ c)
 
-    fixedHeight : IsLattice.FixedHeight isLattice 2
-    fixedHeight = record
-        { ⊥ = ⊥
-        ; ⊤ = ⊤
-        ; longestChain = longestChain
-        ; bounded = isLongest
-        }
+    instance
+        fixedHeight : IsLattice.FixedHeight isLattice 2
+        fixedHeight = record
+            { ⊥ = ⊥
+            ; ⊤ = ⊤
+            ; longestChain = longestChain
+            ; bounded = isLongest
+            }
 
-    isFiniteHeightLattice : IsFiniteHeightLattice AboveBelow 2 _≈_ _⊔_ _⊓_
-    isFiniteHeightLattice = record
-        { isLattice = isLattice
-        ; fixedHeight = fixedHeight
-        }
+        isFiniteHeightLattice : IsFiniteHeightLattice AboveBelow 2 _≈_ _⊔_ _⊓_
+        isFiniteHeightLattice = record
+            { isLattice = isLattice
+            ; fixedHeight = fixedHeight
+            }
 
-    finiteHeightLattice : FiniteHeightLattice AboveBelow
-    finiteHeightLattice = record
-        { height = 2
-        ; _≈_ = _≈_
-        ; _⊔_ = _⊔_
-        ; _⊓_ = _⊓_
-        ; isFiniteHeightLattice = isFiniteHeightLattice
-        }
+        finiteHeightLattice : FiniteHeightLattice AboveBelow
+        finiteHeightLattice = record
+            { height = 2
+            ; _≈_ = _≈_
+            ; _⊔_ = _⊔_
+            ; _⊓_ = _⊓_
+            ; isFiniteHeightLattice = isFiniteHeightLattice
+            }
diff --git a/Lattice/FiniteMap.agda b/Lattice/FiniteMap.agda
index cfd75ca..a90e2c2 100644
--- a/Lattice/FiniteMap.agda
+++ b/Lattice/FiniteMap.agda
@@ -3,15 +3,16 @@ open import Relation.Binary.PropositionalEquality as Eq
     using (_≡_;refl; sym; trans; cong; subst)
 open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
 open import Data.List using (List; _∷_; [])
+open import Data.Unit using (⊤)
 
-module Lattice.FiniteMap {A : Set} {B : Set}
+module Lattice.FiniteMap (A : Set) (B : Set)
     {_≈₂_ : B → B → Set}
     {_⊔₂_ : B → B → B} {_⊓₂_ : B → B → B}
-    (≡-Decidable-A : IsDecidable {_} {A} _≡_)
-    (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
+    {{≡-Decidable-A : IsDecidable {_} {A} _≡_}}
+    {{lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_}} (dummy : ⊤) where
 
 open IsLattice lB using () renaming (_≼_ to _≼₂_)
-open import Lattice.Map ≡-Decidable-A lB as Map
+open import Lattice.Map A B dummy as Map
     using
         ( Map
         ; ⊔-equal-keys
@@ -85,11 +86,12 @@ module WithKeys (ks : List A) where
     _≈_ : FiniteMap → FiniteMap → Set
     _≈_ (m₁ , _) (m₂ , _) = m₁ ≈ᵐ m₂
 
-    ≈₂-Decidable⇒≈-Decidable : IsDecidable _≈₂_ → IsDecidable _≈_
-    ≈₂-Decidable⇒≈-Decidable ≈₂-Decidable = record
-        { R-dec = λ fm₁ fm₂ →  IsDecidable.R-dec (≈ᵐ-Decidable ≈₂-Decidable)
-                                                 (proj₁ fm₁) (proj₁ fm₂)
-        }
+    instance
+        ≈-Decidable : {{ IsDecidable _≈₂_ }} → IsDecidable _≈_
+        ≈-Decidable {{≈₂-Decidable}} = record
+            { R-dec = λ fm₁ fm₂ →  IsDecidable.R-dec (≈ᵐ-Decidable {{≈₂-Decidable}})
+                                                     (proj₁ fm₁) (proj₁ fm₂)
+            }
 
     _⊔_ : FiniteMap → FiniteMap → FiniteMap
     _⊔_ (m₁ , km₁≡ks) (m₂ , km₂≡ks) =
@@ -142,46 +144,47 @@ module WithKeys (ks : List A) where
                 IsEquivalence.≈-trans ≈ᵐ-equiv {m₁} {m₂} {m₃}
         }
 
-    isUnionSemilattice : IsSemilattice FiniteMap _≈_ _⊔_
-    isUnionSemilattice = record
-        { ≈-equiv = ≈-equiv
-        ; ≈-⊔-cong =
-            λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} {(m₄ , _)} m₁≈m₂ m₃≈m₄ →
-                ≈ᵐ-⊔ᵐ-cong {m₁} {m₂} {m₃} {m₄} m₁≈m₂ m₃≈m₄
-        ; ⊔-assoc = λ (m₁ , _) (m₂ , _) (m₃ , _) → ⊔ᵐ-assoc m₁ m₂ m₃
-        ; ⊔-comm = λ (m₁ , _) (m₂ , _) → ⊔ᵐ-comm m₁ m₂
-        ; ⊔-idemp = λ (m , _) → ⊔ᵐ-idemp m
-        }
+    instance
+        isUnionSemilattice : IsSemilattice FiniteMap _≈_ _⊔_
+        isUnionSemilattice = record
+            { ≈-equiv = ≈-equiv
+            ; ≈-⊔-cong =
+                λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} {(m₄ , _)} m₁≈m₂ m₃≈m₄ →
+                    ≈ᵐ-⊔ᵐ-cong {m₁} {m₂} {m₃} {m₄} m₁≈m₂ m₃≈m₄
+            ; ⊔-assoc = λ (m₁ , _) (m₂ , _) (m₃ , _) → ⊔ᵐ-assoc m₁ m₂ m₃
+            ; ⊔-comm = λ (m₁ , _) (m₂ , _) → ⊔ᵐ-comm m₁ m₂
+            ; ⊔-idemp = λ (m , _) → ⊔ᵐ-idemp m
+            }
 
-    isIntersectSemilattice : IsSemilattice FiniteMap _≈_ _⊓_
-    isIntersectSemilattice = record
-        { ≈-equiv = ≈-equiv
-        ; ≈-⊔-cong =
-            λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} {(m₄ , _)} m₁≈m₂ m₃≈m₄ →
-                ≈ᵐ-⊓ᵐ-cong {m₁} {m₂} {m₃} {m₄} m₁≈m₂ m₃≈m₄
-        ; ⊔-assoc = λ (m₁ , _) (m₂ , _) (m₃ , _) → ⊓ᵐ-assoc m₁ m₂ m₃
-        ; ⊔-comm = λ (m₁ , _) (m₂ , _) → ⊓ᵐ-comm m₁ m₂
-        ; ⊔-idemp = λ (m , _) → ⊓ᵐ-idemp m
-        }
+        isIntersectSemilattice : IsSemilattice FiniteMap _≈_ _⊓_
+        isIntersectSemilattice = record
+            { ≈-equiv = ≈-equiv
+            ; ≈-⊔-cong =
+                λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} {(m₄ , _)} m₁≈m₂ m₃≈m₄ →
+                    ≈ᵐ-⊓ᵐ-cong {m₁} {m₂} {m₃} {m₄} m₁≈m₂ m₃≈m₄
+            ; ⊔-assoc = λ (m₁ , _) (m₂ , _) (m₃ , _) → ⊓ᵐ-assoc m₁ m₂ m₃
+            ; ⊔-comm = λ (m₁ , _) (m₂ , _) → ⊓ᵐ-comm m₁ m₂
+            ; ⊔-idemp = λ (m , _) → ⊓ᵐ-idemp m
+            }
 
-    isLattice : IsLattice FiniteMap _≈_ _⊔_ _⊓_
-    isLattice = record
-        { joinSemilattice = isUnionSemilattice
-        ; meetSemilattice = isIntersectSemilattice
-        ; absorb-⊔-⊓ = λ (m₁ , _) (m₂ , _) → absorb-⊔ᵐ-⊓ᵐ m₁ m₂
-        ; absorb-⊓-⊔ = λ (m₁ , _) (m₂ , _) → absorb-⊓ᵐ-⊔ᵐ m₁ m₂
-        }
+        isLattice : IsLattice FiniteMap _≈_ _⊔_ _⊓_
+        isLattice = record
+            { joinSemilattice = isUnionSemilattice
+            ; meetSemilattice = isIntersectSemilattice
+            ; absorb-⊔-⊓ = λ (m₁ , _) (m₂ , _) → absorb-⊔ᵐ-⊓ᵐ m₁ m₂
+            ; absorb-⊓-⊔ = λ (m₁ , _) (m₂ , _) → absorb-⊓ᵐ-⊔ᵐ m₁ m₂
+            }
+
+        lattice : Lattice FiniteMap
+        lattice = record
+            { _≈_ = _≈_
+            ; _⊔_ = _⊔_
+            ; _⊓_ = _⊓_
+            ; isLattice = isLattice
+            }
 
     open IsLattice isLattice using (_≼_; ⊔-Monotonicˡ; ⊔-Monotonicʳ) public
 
-    lattice : Lattice FiniteMap
-    lattice = record
-        { _≈_ = _≈_
-        ; _⊔_ = _⊔_
-        ; _⊓_ = _⊓_
-        ; isLattice = isLattice
-        }
-
     m₁≼m₂⇒m₁[k]≼m₂[k] : ∀ (fm₁ fm₂ : FiniteMap) {k : A} {v₁ v₂ : B} →
                         fm₁ ≼ fm₂ → (k , v₁) ∈ fm₁ → (k , v₂) ∈ fm₂ → v₁ ≼₂ v₂
     m₁≼m₂⇒m₁[k]≼m₂[k] (m₁ , _) (m₂ , _) m₁≼m₂ k,v₁∈m₁ k,v₂∈m₂ = m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ m₁ m₂ m₁≼m₂ k,v₁∈m₁ k,v₂∈m₂
@@ -194,7 +197,7 @@ module WithKeys (ks : List A) where
     module GeneralizedUpdate
              {l} {L : Set l}
              {_≈ˡ_ : L → L → Set l} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L}
-             (lL : IsLattice L _≈ˡ_ _⊔ˡ_ _⊓ˡ_)
+             {{lL : IsLattice L _≈ˡ_ _⊔ˡ_ _⊓ˡ_}}
              (f : L → FiniteMap) (f-Monotonic : Monotonic (IsLattice._≼_ lL) _≼_ f)
              (g : A → L → B) (g-Monotonicʳ : ∀ k → Monotonic (IsLattice._≼_ lL) _≼₂_ (g k))
              (ks : List A) where
@@ -208,7 +211,7 @@ module WithKeys (ks : List A) where
         f' l = (f l) updating ks via (updater l)
 
         f'-Monotonic : Monotonic _≼ˡ_ _≼_ f'
-        f'-Monotonic {l₁} {l₂} l₁≼l₂ = f'-Monotonicᵐ lL (proj₁ ∘ f) f-Monotonic g g-Monotonicʳ ks l₁≼l₂
+        f'-Monotonic {l₁} {l₂} l₁≼l₂ = f'-Monotonicᵐ (proj₁ ∘ f) f-Monotonic g g-Monotonicʳ ks l₁≼l₂
 
         f'-∈k-forward : ∀ {k l} → k ∈k (f l) → k ∈k (f' l)
         f'-∈k-forward {k} {l} = updatingᵐ-via-∈k-forward (proj₁ (f l)) ks (updater l)
@@ -253,7 +256,7 @@ module WithKeys (ks : List A) where
 open WithKeys public
 
 module IterProdIsomorphism where
-    open import Data.Unit using (⊤; tt)
+    open import Data.Unit using (tt)
     open import Lattice.Unit using ()
         renaming
             ( _≈_ to _≈ᵘ_
@@ -264,7 +267,7 @@ module IterProdIsomorphism where
             ; ≈-equiv to ≈ᵘ-equiv
             ; fixedHeight to fixedHeightᵘ
             )
-    open import Lattice.IterProd _≈₂_ _≈ᵘ_ _⊔₂_ _⊔ᵘ_ _⊓₂_ _⊓ᵘ_ lB isLatticeᵘ
+    open import Lattice.IterProd B ⊤ dummy
         as IP
         using (IterProd)
     open IsLattice lB using ()
@@ -299,11 +302,11 @@ module IterProdIsomorphism where
         _⊆ᵐ_ fm₁ fm₂ = subset-impl (proj₁ (proj₁ fm₁)) (proj₁ (proj₁ fm₂))
 
         _≈ⁱᵖ_ : ∀ {n : ℕ} → IterProd n → IterProd n → Set
-        _≈ⁱᵖ_ {n} = IP._≈_ n
+        _≈ⁱᵖ_ {n} = IP._≈_ {n}
 
         _⊔ⁱᵖ_ : ∀ {ks : List A} →
                 IterProd (length ks) → IterProd (length ks) → IterProd (length ks)
-        _⊔ⁱᵖ_ {ks} = IP._⊔_ (length ks)
+        _⊔ⁱᵖ_ {ks} = IP._⊔_ {length ks}
 
         _∈ᵐ_ : ∀ {ks : List A} → A × B → FiniteMap ks → Set
         _∈ᵐ_ {ks} = _∈_ ks
@@ -320,7 +323,7 @@ module IterProdIsomorphism where
     from-to-inverseˡ : ∀ {ks : List A} (uks : Unique ks) →
                       IsInverseˡ (_≈_ ks) (_≈ⁱᵖ_ {length ks})
                                  (from {ks}) (to {ks} uks)
-    from-to-inverseˡ {[]} _ _ = IsEquivalence.≈-refl (IP.≈-equiv 0)
+    from-to-inverseˡ {[]} _ _ = IsEquivalence.≈-refl (IP.≈-equiv {0})
     from-to-inverseˡ {k ∷ ks'} (push k≢ks' uks') (v , rest)
         with ((fm' , ufm') , refl) ← to uks' rest in p rewrite sym p =
             (IsLattice.≈-refl lB , from-to-inverseˡ {ks'} uks' rest)
@@ -522,7 +525,7 @@ module IterProdIsomorphism where
 
             fm₂⊆fm₁ : to uks ip₂ ⊆ᵐ to uks ip₁
             fm₂⊆fm₁ = inductive-step (≈₂-sym v₁≈v₂)
-                                     (IP.≈-sym (length ks') rest₁≈rest₂)
+                                     (IP.≈-sym {length ks'} rest₁≈rest₂)
 
     from-⊔-distr : ∀ {ks : List A} → (fm₁ fm₂ : FiniteMap ks) →
                   _≈ⁱᵖ_ {length ks} (from (_⊔_ _ fm₁ fm₂))
@@ -545,7 +548,7 @@ module IterProdIsomorphism where
                 rewrite from-rest (_⊔_ _ fm₁ fm₂) rewrite from-rest fm₁ rewrite from-rest fm₂
                 = ( IsLattice.≈-refl lB
                   , IsEquivalence.≈-trans
-                        (IP.≈-equiv (length ks))
+                        (IP.≈-equiv {length ks})
                         (from-preserves-≈ {_} {pop (_⊔_ _ fm₁ fm₂)}
                                               {_⊔_ _ (pop fm₁) (pop fm₂)}
                                               (pop-⊔-distr fm₁ fm₂))
@@ -610,15 +613,15 @@ module IterProdIsomorphism where
                         in
                             (v' , (v₁⊔v₂≈v' , there v'∈fm'))
 
-    module WithUniqueKeysAndFixedHeight {ks : List A} (uks : Unique ks) (≈₂-Decidable : IsDecidable _≈₂_) (h₂ : ℕ) (fhB : FixedHeight₂ h₂) where
+    module WithUniqueKeysAndFixedHeight {ks : List A} (uks : Unique ks) {{≈₂-Decidable : IsDecidable _≈₂_}} {h₂ : ℕ} {{fhB : FixedHeight₂ h₂}} where
         import Isomorphism
         open Isomorphism.TransportFiniteHeight
-            (IP.isFiniteHeightLattice (length ks) ≈₂-Decidable ≈ᵘ-Decidable h₂ 0 fhB fixedHeightᵘ) (isLattice ks)
+            (IP.isFiniteHeightLattice {k = length ks} {{fhB = fixedHeightᵘ}}) (isLattice ks)
             {f = to uks} {g = from {ks}}
             (to-preserves-≈ uks) (from-preserves-≈ {ks})
             (to-⊔-distr uks) (from-⊔-distr {ks})
             (from-to-inverseʳ uks) (from-to-inverseˡ uks)
-            using (isFiniteHeightLattice; finiteHeightLattice) public
+            using (isFiniteHeightLattice; finiteHeightLattice; fixedHeight) public
 
         -- Helpful lemma: all entries of the 'bottom' map are assigned to bottom.
 
@@ -626,5 +629,5 @@ module IterProdIsomorphism where
 
         ⊥-contains-bottoms : ∀ {k : A} {v : B} → (k , v) ∈ᵐ ⊥ → v ≡ (Height.⊥ fhB)
         ⊥-contains-bottoms {k} {v} k,v∈⊥
-            rewrite IP.⊥-built (length ks) ≈₂-Decidable ≈ᵘ-Decidable h₂ 0 fhB fixedHeightᵘ =
+            rewrite IP.⊥-built {length ks} {{fhB = fixedHeightᵘ}} =
             to-build uks k v k,v∈⊥
diff --git a/Lattice/IterProd.agda b/Lattice/IterProd.agda
index 37718e4..a3e3acb 100644
--- a/Lattice/IterProd.agda
+++ b/Lattice/IterProd.agda
@@ -1,14 +1,15 @@
 open import Lattice
+open import Data.Unit using (⊤)
 
 -- Due to universe levels, it becomes relatively annoying to handle the case
 -- where the levels of A and B are not the same. For the time being, constrain
 -- them to be the same.
 
-module Lattice.IterProd {a} {A B : Set a}
-    (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a)
-    (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B)
-    (_⊓₁_ : A → A → A) (_⊓₂_ : B → B → B)
-    (lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
+module Lattice.IterProd {a} (A B : Set a)
+    {_≈₁_ : A → A → Set a} {_≈₂_ : B → B → Set a}
+    {_⊔₁_ : A → A → A} {_⊔₂_ : B → B → B}
+    {_⊓₁_ : A → A → A} {_⊓₂_ : B → B → B}
+    {{lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_}} {{lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_}} (dummy : ⊤) where
 
 open import Agda.Primitive using (lsuc)
 open import Data.Nat using (ℕ; zero; suc; _+_)
@@ -119,49 +120,55 @@ private
                 _⊓₁_ (Everything._⊓_ everythingRest)
                 lA  (Everything.isLattice everythingRest) as P
 
-module _ (k : ℕ) where
-    open Everything (everything k) using (_≈_; _⊔_; _⊓_; isLattice) public
-    open Lattice.IsLattice isLattice public
+module _ {k : ℕ} where
+    open Everything (everything k) using (_≈_; _⊔_; _⊓_) public
+    open Lattice.IsLattice (Everything.isLattice (everything k)) public
 
-    lattice : Lattice (IterProd k)
-    lattice = record
-        { _≈_ = _≈_
-        ; _⊔_ = _⊔_
-        ; _⊓_ = _⊓_
-        ; isLattice = isLattice
-        }
+    instance
+        isLattice = Everything.isLattice (everything k)
 
-    module _ (≈₁-Decidable : IsDecidable _≈₁_) (≈₂-Decidable : IsDecidable _≈₂_)
-             (h₁ h₂ : ℕ)
-             (fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where
-
-        private
-            required : RequiredForFixedHeight
-            required = record
-                { ≈₁-Decidable = ≈₁-Decidable
-                ; ≈₂-Decidable = ≈₂-Decidable
-                ; h₁ = h₁
-                ; h₂ = h₂
-                ; fhA = fhA
-                ; fhB = fhB
-                }
-
-        fixedHeight = IsFiniteHeightWithBotAndDecEq.fixedHeight (Everything.isFiniteHeightIfSupported (everything k) required)
-
-        isFiniteHeightLattice = record
-            { isLattice = isLattice
-            ; fixedHeight = fixedHeight
-            }
-
-        finiteHeightLattice : FiniteHeightLattice (IterProd k)
-        finiteHeightLattice = record
-            { height = IsFiniteHeightWithBotAndDecEq.height (Everything.isFiniteHeightIfSupported (everything k) required)
-            ; _≈_ = _≈_
+        lattice : Lattice (IterProd k)
+        lattice = record
+            { _≈_ = _≈_
             ; _⊔_ = _⊔_
             ; _⊓_ = _⊓_
-            ; isFiniteHeightLattice = isFiniteHeightLattice
+            ; isLattice = isLattice
             }
 
-        ⊥-built : Height.⊥ fixedHeight ≡ (build (Height.⊥ fhA) (Height.⊥ fhB) k)
-        ⊥-built = IsFiniteHeightWithBotAndDecEq.⊥-correct (Everything.isFiniteHeightIfSupported (everything k) required)
+    module _ {{≈₁-Decidable : IsDecidable _≈₁_}} {{≈₂-Decidable : IsDecidable _≈₂_}}
+             {h₁ h₂ : ℕ}
+             {{fhA : FixedHeight₁ h₁}} {{fhB : FixedHeight₂ h₂}} where
+
+        private
+            isFiniteHeightWithBotAndDecEq =
+                Everything.isFiniteHeightIfSupported (everything k)
+                    record
+                        { ≈₁-Decidable = ≈₁-Decidable
+                        ; ≈₂-Decidable = ≈₂-Decidable
+                        ; h₁ = h₁
+                        ; h₂ = h₂
+                        ; fhA = fhA
+                        ; fhB = fhB
+                        }
+        open IsFiniteHeightWithBotAndDecEq isFiniteHeightWithBotAndDecEq using (height; ⊥-correct)
+
+        instance
+            fixedHeight = IsFiniteHeightWithBotAndDecEq.fixedHeight isFiniteHeightWithBotAndDecEq
+
+            isFiniteHeightLattice = record
+                { isLattice = isLattice
+                ; fixedHeight = fixedHeight
+                }
+
+            finiteHeightLattice : FiniteHeightLattice (IterProd k)
+            finiteHeightLattice = record
+                { height = height
+                ; _≈_ = _≈_
+                ; _⊔_ = _⊔_
+                ; _⊓_ = _⊓_
+                ; isFiniteHeightLattice = isFiniteHeightLattice
+                }
+
+        ⊥-built : Height.⊥ fixedHeight ≡ (build (Height.⊥ fhA) (Height.⊥ fhB) k)
+        ⊥-built = ⊥-correct
 
diff --git a/Lattice/Map.agda b/Lattice/Map.agda
index 0dbc4a6..084afd7 100644
--- a/Lattice/Map.agda
+++ b/Lattice/Map.agda
@@ -1,12 +1,14 @@
 open import Lattice
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst)
 open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
+open import Data.Unit using (⊤)
 
-module Lattice.Map {a b : Level} {A : Set a} {B : Set b}
+module Lattice.Map {a b : Level} (A : Set a) (B : Set b)
     {_≈₂_ : B → B → Set b}
     {_⊔₂_ : B → B → B} {_⊓₂_ : B → B → B}
-    (≡-Decidable-A : IsDecidable {a} {A} _≡_)
-    (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
+    {{≡-Decidable-A : IsDecidable {a} {A} _≡_}}
+    {{lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_}}
+    (dummy : ⊤) where
 
 open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_)
 
@@ -626,7 +628,7 @@ Expr-Provenance-≡ {k} {v} e k,v∈e
     with (v' , (p , k,v'∈e)) ← Expr-Provenance k e (forget k,v∈e)
     rewrite Map-functional {m = ⟦ e ⟧} k,v∈e k,v'∈e = p
 
-module _ (≈₂-Decidable : IsDecidable _≈₂_) where
+module _ {{≈₂-Decidable : IsDecidable _≈₂_}} where
     open IsDecidable ≈₂-Decidable using () renaming (R-dec to ≈₂-dec)
     private module _ where
         data SubsetInfo (m₁ m₂ : Map) : Set (a ⊔ℓ b) where
@@ -1031,7 +1033,7 @@ updating-via-k∉ks-backward m = transform-k∉ks-backward
 
 module _ {l} {L : Set l}
          {_≈ˡ_ : L → L → Set l} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L}
-         (lL : IsLattice L _≈ˡ_ _⊔ˡ_ _⊓ˡ_) where
+         {{lL : IsLattice L _≈ˡ_ _⊔ˡ_ _⊓ˡ_}} where
     open IsLattice lL using () renaming (_≼_ to _≼ˡ_)
 
     module _ (f : L → Map) (f-Monotonic : Monotonic _≼ˡ_ _≼_ f)
diff --git a/Lattice/MapSet.agda b/Lattice/MapSet.agda
index 2b44a2a..9737377 100644
--- a/Lattice/MapSet.agda
+++ b/Lattice/MapSet.agda
@@ -1,8 +1,9 @@
 open import Lattice
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst)
 open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
+open import Data.Unit using (⊤)
 
-module Lattice.MapSet {a : Level} {A : Set a} (≡-Decidable-A : IsDecidable (_≡_ {a} {A})) where
+module Lattice.MapSet {a : Level} (A : Set a) {{≡-Decidable-A : IsDecidable (_≡_ {a} {A})}} (dummy : ⊤) where
 
 open import Data.List using (List; map)
 open import Data.Product using (_,_; proj₁)
@@ -11,7 +12,7 @@ open import Function using (_∘_)
 open import Lattice.Unit using (⊤; tt) renaming (_≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_; isLattice to ⊤-isLattice)
 import Lattice.Map
 
-private module UnitMap = Lattice.Map ≡-Decidable-A ⊤-isLattice
+private module UnitMap = Lattice.Map A ⊤ dummy
 open UnitMap
     using (Map; Expr; ⟦_⟧)
     renaming
diff --git a/Lattice/Unit.agda b/Lattice/Unit.agda
index 16cc0fd..c92d512 100644
--- a/Lattice/Unit.agda
+++ b/Lattice/Unit.agda
@@ -28,8 +28,9 @@ _≈_ = _≡_
 ≈-dec : Decidable _≈_
 ≈-dec = _≟_
 
-≈-Decidable : IsDecidable _≈_
-≈-Decidable = record { R-dec = ≈-dec }
+instance
+    ≈-Decidable : IsDecidable _≈_
+    ≈-Decidable = record { R-dec = ≈-dec }
 
 _⊔_ : ⊤ → ⊤ → ⊤
 tt ⊔ tt = tt
diff --git a/Utils.agda b/Utils.agda
index ea6b88c..33f8045 100644
--- a/Utils.agda
+++ b/Utils.agda
@@ -103,3 +103,6 @@ _∨_ P Q a = P a ⊎ Q a
 _∧_ : ∀ {a p₁ p₂} {A : Set a} (P : A → Set p₁) (Q : A → Set p₂) →
       A → Set (p₁ ⊔ℓ p₂)
 _∧_ P Q a = P a × Q a
+
+it : ∀ {a} {A : Set a} {{_ : A}} → A
+it {{x}} = x