Switch maps (and consequently most of the code) to using instances

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2025-01-04 21:16:22 -08:00
parent d90b544436
commit d96eb97b69
16 changed files with 257 additions and 240 deletions
--- 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
+            }
--- 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∈⊥
--- 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

--- 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)
--- 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
--- 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