Switch product to using instances

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
Swich AboveBelow to using instances
2025-01-04 21:33:59 -08:00 · 2025-01-04 21:23:07 -08:00 · 2025-01-04 21:16:22 -08:00 · 2025-01-04 19:08:28 -08:00 · 2025-01-04 18:58:56 -08:00 · 2025-01-04 17:27:38 -08:00
19 changed files with 538 additions and 482 deletions
--- 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
@ -65,7 +65,7 @@ module WithProg (prog : Program) where
                           (joinAll-Mono {sv₁} {sv₂} sv₁≼sv₂)

        -- The fixed point of the 'analyze' function is our final goal.
-        open import Fixedpoint ≈ᵐ-dec isFiniteHeightLatticeᵐ analyze (λ {m₁} {m₂} m₁≼m₂ → analyze-Mono {m₁} {m₂} m₁≼m₂)
+        open import Fixedpoint ≈ᵐ-Decidable isFiniteHeightLatticeᵐ analyze (λ {m₁} {m₂} m₁≼m₂ → analyze-Mono {m₁} {m₂} m₁≼m₂)
            using ()
            renaming (aᶠ to result; aᶠ≈faᶠ to result≈analyze-result)
            public
--- 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
--- 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ˡ
--- 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 _≈ˡ_ _⊔ˡ_ _⊓ˡ_)
-    (≈ˡ-dec : 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,11 +30,15 @@ open Program prog
 import Lattice.FiniteMap
 import Chain

+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 _≟ˢ_ isLatticeˡ vars
+module VariableValuesFiniteMap = Lattice.FiniteMap.WithKeys String L tt vars
 open VariableValuesFiniteMap
    using ()
    renaming
@ -42,7 +47,7 @@ open VariableValuesFiniteMap
        ; _≈_ to _≈ᵛ_
        ; _⊔_ to _⊔ᵛ_
        ; _≼_ to _≼ᵛ_
-        ; ≈₂-dec⇒≈-dec to ≈ˡ-dec⇒≈ᵛ-dec
+        ; ≈-Decidable to ≈ᵛ-Decidable
        ; _∈_ to _∈ᵛ_
        ; _∈k_ to _∈kᵛ_
        ; _updating_via_ to _updatingᵛ_via_
@ -60,27 +65,25 @@ open IsLattice isLatticeᵛ
        ; ⊔-idemp to ⊔ᵛ-idemp
        )
    public
-open Lattice.FiniteMap.IterProdIsomorphism _≟ˢ_ isLatticeˡ
+open Lattice.FiniteMap.IterProdIsomorphism String L _
    using ()
    renaming
        ( Provenance-union to Provenance-unionᵐ
        )
    public
-open Lattice.FiniteMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight _≟ˢ_ isLatticeˡ vars-Unique ≈ˡ-dec _ fixedHeightˡ
+open Lattice.FiniteMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight String L _ vars-Unique
    using ()
    renaming
        ( isFiniteHeightLattice to isFiniteHeightLatticeᵛ
+        ; fixedHeight to fixedHeightᵛ
        ; ⊥-contains-bottoms to ⊥ᵛ-contains-bottoms
        )
    public

-≈ᵛ-dec = ≈ˡ-dec⇒≈ᵛ-dec ≈ˡ-dec
-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 _≟_ 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
@ -91,11 +94,11 @@ open StateVariablesFiniteMap
        ; _∈k_ to _∈kᵐ_
        ; locate to locateᵐ
        ; _≼_ to _≼ᵐ_
-        ; ≈₂-dec⇒≈-dec to ≈ᵛ-dec⇒≈ᵐ-dec
+        ; ≈-Decidable to ≈ᵐ-Decidable
        ; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ
        )
    public
-open Lattice.FiniteMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight _≟_ isLatticeᵛ states-Unique ≈ᵛ-dec _ fixedHeightᵛ
+open Lattice.FiniteMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight State VariableValues _ states-Unique
    using ()
    renaming
        ( isFiniteHeightLattice to isFiniteHeightLatticeᵐ
@ -108,9 +111,6 @@ open IsFiniteHeightLattice isFiniteHeightLatticeᵐ
        )
    public

-≈ᵐ-dec = ≈ᵛ-dec⇒≈ᵐ-dec ≈ᵛ-dec
-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
@ -144,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
--- a/Analysis/Sign.agda
+++ b/Analysis/Sign.agda
@ -7,11 +7,13 @@ open import Data.Sum using (inj₁; inj₂)
 open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Unit using (⊤; tt)
 open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_)
+open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; subst)
 open import Relation.Nullary using (¬_; yes; no)

 open import Language
 open import Lattice
+open import Equivalence
 open import Showable using (Showable; show)
 open import Utils using (_⇒_; _∧_; _∨_)
 import Analysis.Forward
@ -32,7 +34,7 @@ instance
        }

 -- g for siGn; s is used for strings and i is not very descriptive.
-_≟ᵍ_ : IsDecidable (_≡_ {_} {Sign})
+_≟ᵍ_ : Decidable (_≡_ {_} {Sign})
 _≟ᵍ_ + + = yes refl
 _≟ᵍ_ + - = no (λ ())
 _≟ᵍ_ + 0ˢ = no (λ ())
@ -43,12 +45,22 @@ _≟ᵍ_ 0ˢ + = no (λ ())
 _≟ᵍ_ 0ˢ - = no (λ ())
 _≟ᵍ_ 0ˢ 0ˢ = yes refl

+instance
+    ≡-equiv : IsEquivalence Sign _≡_
+    ≡-equiv = record
+        { ≈-refl = refl
+        ; ≈-sym = sym
+        ; ≈-trans = trans
+        }
+
+    ≡-Decidable-Sign : IsDecidable {_} {Sign} _≡_
+    ≡-Decidable-Sign = record { R-dec = _≟ᵍ_ }
+
 -- embelish 'sign' with a top and bottom element.
-open import Lattice.AboveBelow Sign _≡_ (record { ≈-refl = refl; ≈-sym = sym; ≈-trans = trans }) _≟ᵍ_ as AB
+open import Lattice.AboveBelow Sign _ as AB
    using ()
    renaming
        ( AboveBelow to SignLattice
-        ; ≈-dec to ≈ᵍ-dec
        ; ⊥ to ⊥ᵍ
        ; ⊤ to ⊤ᵍ
        ; [_] to [_]ᵍ
@ -68,10 +80,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 ⊥ᵍ _ = ⊥ᵍ
@ -171,9 +180,9 @@ instance
 module WithProg (prog : Program) where
    open Program prog

-    open import Analysis.Forward.Lattices isFiniteHeightLatticeᵍ ≈ᵍ-dec prog
-    open import Analysis.Forward.Evaluation isFiniteHeightLatticeᵍ ≈ᵍ-dec prog
-    open import Analysis.Forward.Adapters isFiniteHeightLatticeᵍ ≈ᵍ-dec 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)
@ -229,7 +238,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ᵍ ≈ᵍ-dec 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
--- 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}
-                  (≈-dec : IsDecidable _≈_)
+                  (≈-Decidable : IsDecidable _≈_)
                  (flA : IsFiniteHeightLattice A h _≈_ _⊔_ _⊓_)
                  (f : A → A)
                  (Monotonicᶠ : Monotonic (IsFiniteHeightLattice._≼_ flA)
@ -17,6 +17,7 @@ open import Data.Empty using (⊥-elim)
 open import Relation.Binary.PropositionalEquality using (_≡_; sym)
 open import Relation.Nullary using (Dec; ¬_; yes; no)

+open IsDecidable ≈-Decidable using () renaming (R-dec to ≈-dec)
 open IsFiniteHeightLattice flA

 import Chain
--- 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
+            }
--- a/Language.agda
+++ b/Language.agda
@ -16,12 +16,13 @@ open import Data.Nat using (ℕ; suc)
 open import Data.Product using (_,_; Σ; proj₁; proj₂)
 open import Data.Product.Properties as ProdProp using ()
 open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
+open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl)
 open import Relation.Nullary using (¬_)

 open import Lattice
 open import Utils using (Unique; push; Unique-map; x∈xs⇒fx∈fxs)
-open import Lattice.MapSet _≟ˢ_ using ()
+open import Lattice.MapSet String {{record { R-dec = _≟ˢ_ }}} _ using ()
    renaming
        ( MapSet to StringSet
        ; to-List to to-Listˢ
@ -73,10 +74,10 @@ record Program : Set where
    -- vars-complete : ∀ {k : String} (s : State) → k ∈ᵇ (code s) → k ListMem.∈ vars
    -- vars-complete {k} s = ∈⇒∈-Stmts-vars {length} {k} {stmts} {s}

-    _≟_ : IsDecidable (_≡_ {_} {State})
+    _≟_ : Decidable (_≡_ {_} {State})
    _≟_ = FinProp._≟_

-    _≟ᵉ_ : IsDecidable (_≡_ {_} {Graph.Edge graph})
+    _≟ᵉ_ : Decidable (_≡_ {_} {Graph.Edge graph})
    _≟ᵉ_ = ProdProp.≡-dec _≟_ _≟_

    open import Data.List.Membership.DecPropositional _≟ᵉ_ using (_∈?_)
--- 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 (String._≟_)
+open import Lattice.MapSet String {{record { R-dec = String._≟_ }}} _
    renaming
        ( MapSet to StringSet
        ; insert to insertˢ
--- a/Lattice.agda
+++ b/Lattice.agda
@ -11,8 +11,9 @@ open import Data.Sum using (_⊎_; inj₁; inj₂)
 open import Agda.Primitive using (lsuc; Level) renaming (_⊔_ to _⊔ℓ_)
 open import Function.Definitions using (Injective)

-IsDecidable : ∀ {a} {A : Set a} (R : A → A → Set a) → Set a
-IsDecidable {a} {A} R = ∀ (a₁ a₂ : A) → Dec (R a₁ a₂)
+record IsDecidable {a} {A : Set a} (R : A → A → Set a) : Set a where
+    field
+        R-dec : ∀ (a₁ a₂ : A) → Dec (R a₁ a₂)

 module _ {a b} {A : Set a} {B : Set b}
    (_≼₁_ : A → A → Set a) (_≼₂_ : B → B → Set b) where
@ -186,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
@ -216,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}
@ -251,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

@ -262,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

@ -273,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
--- a/Lattice/AboveBelow.agda
+++ b/Lattice/AboveBelow.agda
@ -1,17 +1,19 @@
 open import Lattice
 open import Equivalence
 open import Relation.Nullary using (Dec; ¬_; yes; no)
+open import Data.Unit using () renaming (⊤ to ⊤ᵘ)

 module Lattice.AboveBelow {a} (A : Set a)
-                          (_≈₁_ : A → A → Set a)
-                          (≈₁-equiv : IsEquivalence A _≈₁_)
-                          (≈₁-dec : IsDecidable _≈₁_) where
+                          {_≈₁_ : A → A → Set a}
+                          {{≈₁-equiv : IsEquivalence A _≈₁_}}
+                          {{≈₁-Decidable : IsDecidable _≈₁_}} (dummy : ⊤ᵘ) where

 open import Data.Empty using (⊥-elim)
 open import Data.Product using (_,_)
 open import Data.Nat using (_≤_; ℕ; z≤n; s≤s; suc)
 open import Function using (_∘_)
 open import Showable using (Showable; show)
+open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Binary.PropositionalEquality as Eq
    using (_≡_; sym; subst; refl)

@ -20,6 +22,8 @@ import Chain
 open IsEquivalence ≈₁-equiv using ()
    renaming (≈-refl to ≈₁-refl; ≈-sym to ≈₁-sym; ≈-trans to ≈₁-trans)

+open IsDecidable ≈₁-Decidable using () renaming (R-dec to ≈₁-dec)
+
 data AboveBelow : Set a where
    ⊥ : AboveBelow
    ⊤ : AboveBelow
@ -62,7 +66,7 @@ data _≈_ : AboveBelow → AboveBelow → Set a where
    ; ≈-trans = ≈-trans
    }

-≈-dec : IsDecidable _≈_
+≈-dec : Decidable _≈_
 ≈-dec ⊥ ⊥ = yes ≈-⊥-⊥
 ≈-dec ⊤ ⊤ = yes ≈-⊤-⊤
 ≈-dec [ x ] [ y ]
@ -76,6 +80,10 @@ data _≈_ : AboveBelow → AboveBelow → Set a where
 ≈-dec [ x ] ⊥ = no λ ()
 ≈-dec [ x ] ⊤ = no λ ()

+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
 -- unordered. That's what this module does.
@ -169,14 +177,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 = ⊥
@ -262,14 +271,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₂ = ≈-⊥-⊥
@ -294,21 +304,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

@ -354,25 +365,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}
-    (≡-dec-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 ≡-dec-A lB as Map
+open import Lattice.Map A B dummy as Map
    using
        ( Map
        ; ⊔-equal-keys
@ -39,7 +40,7 @@ open import Lattice.Map ≡-dec-A lB as Map
        ; ⊓-idemp to ⊓ᵐ-idemp
        ; absorb-⊔-⊓ to absorb-⊔ᵐ-⊓ᵐ
        ; absorb-⊓-⊔ to absorb-⊓ᵐ-⊔ᵐ
-        ; ≈-dec to ≈ᵐ-dec
+        ; ≈-Decidable to ≈ᵐ-Decidable
        ; _[_] to _[_]ᵐ
        ; []-∈ to []ᵐ-∈
        ; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ
@ -67,7 +68,6 @@ open import Data.Nat using (ℕ)
 open import Data.Product using (_×_; _,_; Σ; proj₁; proj₂)
 open import Equivalence
 open import Function using (_∘_)
-open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Utils using (Pairwise; _∷_; []; Unique; push; empty; All¬-¬Any)
 open import Showable using (Showable; show)
@ -86,8 +86,12 @@ module WithKeys (ks : List A) where
    _≈_ : FiniteMap → FiniteMap → Set
    _≈_ (m₁ , _) (m₂ , _) = m₁ ≈ᵐ m₂

-    ≈₂-dec⇒≈-dec : IsDecidable _≈₂_ → IsDecidable _≈_
-    ≈₂-dec⇒≈-dec ≈₂-dec fm₁ fm₂ = ≈ᵐ-dec ≈₂-dec (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) =
@ -140,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₂
@ -192,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
@ -206,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)
@ -251,18 +256,18 @@ 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 _≈ᵘ_
            ; _⊔_ to _⊔ᵘ_
            ; _⊓_ to _⊓ᵘ_
-            ; ≈-dec to ≈ᵘ-dec
+            ; ≈-Decidable to ≈ᵘ-Decidable
            ; isLattice to isLatticeᵘ
            ; ≈-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 ()
@ -297,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
@ -318,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)
@ -520,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₂))
@ -543,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₂))
@ -608,15 +613,15 @@ module IterProdIsomorphism where
                        in
                            (v' , (v₁⊔v₂≈v' , there v'∈fm'))

-    module WithUniqueKeysAndFixedHeight {ks : List A} (uks : Unique ks) (≈₂-dec : Decidable _≈₂_) (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) ≈₂-dec ≈ᵘ-dec 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.

@ -624,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) ≈₂-dec ≈ᵘ-dec 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; _+_)
@ -39,11 +40,11 @@ build a b (suc s) = (a , build a b s)
 private
    record RequiredForFixedHeight : Set (lsuc a) where
        field
-            ≈₁-dec : IsDecidable _≈₁_
-            ≈₂-dec : IsDecidable _≈₂_
+            {{≈₁-Decidable}} : IsDecidable _≈₁_
+            {{≈₂-Decidable}} : IsDecidable _≈₂_
            h₁ h₂ : ℕ
-            fhA : FixedHeight₁ h₁
-            fhB : FixedHeight₂ h₂
+            {{fhA}} : FixedHeight₁ h₁
+            {{fhB}} : FixedHeight₂ h₂

        ⊥₁ : A
        ⊥₁ = Height.⊥ fhA
@ -58,7 +59,7 @@ private
        field
            height : ℕ
            fixedHeight : IsLattice.FixedHeight isLattice height
-            ≈-dec : IsDecidable _≈_
+            ≈-Decidable : IsDecidable _≈_

            ⊥-correct : Height.⊥ fixedHeight ≡ ⊥

@ -84,7 +85,7 @@ private
        ; isFiniteHeightIfSupported = λ req → record
            { height = RequiredForFixedHeight.h₂ req
            ; fixedHeight = RequiredForFixedHeight.fhB req
-            ; ≈-dec = RequiredForFixedHeight.≈₂-dec req
+            ; ≈-Decidable = RequiredForFixedHeight.≈₂-Decidable req
            ; ⊥-correct = refl
            }
        }
@ -101,10 +102,9 @@ private
                    { height = (RequiredForFixedHeight.h₁ req) + IsFiniteHeightWithBotAndDecEq.height fhlRest
                    ; fixedHeight =
                        P.fixedHeight
-                        (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightWithBotAndDecEq.≈-dec fhlRest)
-                        (RequiredForFixedHeight.h₁ req) (IsFiniteHeightWithBotAndDecEq.height fhlRest)
-                        (RequiredForFixedHeight.fhA req) (IsFiniteHeightWithBotAndDecEq.fixedHeight fhlRest)
-                    ; ≈-dec = P.≈-dec (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightWithBotAndDecEq.≈-dec fhlRest)
+                            {{≈₂-Decidable = IsFiniteHeightWithBotAndDecEq.≈-Decidable fhlRest}}
+                            {{fhB = IsFiniteHeightWithBotAndDecEq.fixedHeight fhlRest}}
+                    ; ≈-Decidable = P.≈-Decidable {{≈₂-Decidable = IsFiniteHeightWithBotAndDecEq.≈-Decidable fhlRest}}
                    ; ⊥-correct =
                        cong ((Height.⊥ (RequiredForFixedHeight.fhA req)) ,_)
                             (IsFiniteHeightWithBotAndDecEq.⊥-correct fhlRest)
@ -112,56 +112,57 @@ private
        }
        where
            everythingRest = everything k'
+            import Lattice.Prod A (IterProd k') {{lB = Everything.isLattice everythingRest}} as P

-            import Lattice.Prod
-                _≈₁_ (Everything._≈_ everythingRest)
-                _⊔₁_ (Everything._⊔_ everythingRest)
-                _⊓₁_ (Everything._⊓_ everythingRest)
-                lA  (Everything.isLattice everythingRest) as P
+module _ {k : ℕ} where
+    open Everything (everything k) using (_≈_; _⊔_; _⊓_) public
+    open Lattice.IsLattice (Everything.isLattice (everything k)) public

-module _ (k : ℕ) where
-    open Everything (everything k) using (_≈_; _⊔_; _⊓_; isLattice) public
-    open Lattice.IsLattice isLattice public
+    instance
+        isLattice = Everything.isLattice (everything k)

-    lattice : Lattice (IterProd k)
-    lattice = record
-        { _≈_ = _≈_
-        ; _⊔_ = _⊔_
-        ; _⊓_ = _⊓_
-        ; isLattice = isLattice
-        }
-
-    module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
-             (h₁ h₂ : ℕ)
-             (fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where
-
-        private
-            required : RequiredForFixedHeight
-            required = record
-                { ≈₁-dec = ≈₁-dec
-                ; ≈₂-dec = ≈₂-dec
-                ; 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,13 +1,14 @@
 open import Lattice
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst)
-open import Relation.Binary.Definitions using (Decidable)
 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}
-    (≡-dec-A : Decidable (_≡_ {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 _∈ˡ_)

@ -23,6 +24,8 @@ 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 _≟ᴬ_)
+
 open IsLattice lB using () renaming
    ( ≈-refl to ≈₂-refl; ≈-sym to ≈₂-sym; ≈-trans to ≈₂-trans
    ; ≈-⊔-cong to ≈₂-⊔₂-cong; ≈-⊓-cong to ≈₂-⊓₂-cong
@ -41,7 +44,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)
@ -76,7 +79,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)
@ -113,7 +116,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

@ -123,11 +126,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)

@ -135,7 +138,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)))
@ -171,7 +174,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)))

@ -180,9 +183,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'')
@ -193,18 +196,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)

@ -236,11 +239,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)

@ -259,7 +262,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₂
@ -270,11 +273,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)

@ -288,13 +291,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

@ -314,7 +317,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

@ -431,11 +434,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)

@ -449,11 +452,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)

@ -467,7 +470,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'

@ -625,7 +628,8 @@ 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 _ (≈₂-dec : 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
            extra : (k : A) → k ∈k m₁ → ¬ k ∈k m₂ → SubsetInfo m₁ m₂
@ -676,6 +680,9 @@ module _ (≈₂-dec : IsDecidable _≈₂_) where
    ...   | _         | no  m₂̷⊆m₁ = no (λ (_ , m₂⊆m₁) → m₂̷⊆m₁ m₂⊆m₁)
    ...   | no  m₁̷⊆m₂ | _         = no (λ (m₁⊆m₂ , _) → m₁̷⊆m₂ m₁⊆m₂)

+    ≈-Decidable : IsDecidable _≈_
+    ≈-Decidable = record { R-dec = ≈-dec }
+
 private module I⊔ = ImplInsert _⊔₂_
 private module I⊓ = ImplInsert _⊓₂_

@ -1026,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,9 +1,9 @@
 open import Lattice
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst)
-open import Relation.Binary.Definitions using (Decidable)
 open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
+open import Data.Unit using (⊤)

-module Lattice.MapSet {a : Level} {A : Set a} (≡-dec-A : Decidable (_≡_ {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₁)
@ -12,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 ≡-dec-A ⊤-isLattice
+private module UnitMap = Lattice.Map A ⊤ dummy
 open UnitMap
    using (Map; Expr; ⟦_⟧)
    renaming
--- a/Lattice/Nat.agda
+++ b/Lattice/Nat.agda
@ -18,31 +18,32 @@ private
    ≡-⊓-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≡ a₂ → a₃ ≡ a₄ → (a₁ ⊓ a₃) ≡ (a₂ ⊓ a₄)
    ≡-⊓-cong a₁≡a₂ a₃≡a₄ rewrite a₁≡a₂ rewrite a₃≡a₄ = refl

-isMaxSemilattice : IsSemilattice ℕ _≡_ _⊔_
-isMaxSemilattice = record
-    { ≈-equiv = record
-        { ≈-refl = refl
-        ; ≈-sym = sym
-        ; ≈-trans = trans
+instance
+    isMaxSemilattice : IsSemilattice ℕ _≡_ _⊔_
+    isMaxSemilattice = record
+        { ≈-equiv = record
+            { ≈-refl = refl
+            ; ≈-sym = sym
+            ; ≈-trans = trans
+            }
+        ; ≈-⊔-cong = ≡-⊔-cong
+        ; ⊔-assoc = ⊔-assoc
+        ; ⊔-comm = ⊔-comm
+        ; ⊔-idemp = ⊔-idem
        }
-    ; ≈-⊔-cong = ≡-⊔-cong
-    ; ⊔-assoc = ⊔-assoc
-    ; ⊔-comm = ⊔-comm
-    ; ⊔-idemp = ⊔-idem
-    }

-isMinSemilattice : IsSemilattice ℕ _≡_ _⊓_
-isMinSemilattice = record
-    { ≈-equiv = record
-        { ≈-refl = refl
-        ; ≈-sym = sym
-        ; ≈-trans = trans
+    isMinSemilattice : IsSemilattice ℕ _≡_ _⊓_
+    isMinSemilattice = record
+        { ≈-equiv = record
+            { ≈-refl = refl
+            ; ≈-sym = sym
+            ; ≈-trans = trans
+            }
+        ; ≈-⊔-cong = ≡-⊓-cong
+        ; ⊔-assoc = ⊓-assoc
+        ; ⊔-comm = ⊓-comm
+        ; ⊔-idemp = ⊓-idem
        }
-    ; ≈-⊔-cong = ≡-⊓-cong
-    ; ⊔-assoc = ⊓-assoc
-    ; ⊔-comm = ⊓-comm
-    ; ⊔-idemp = ⊓-idem
-    }

 private
    max-bound₁ : {x y z : ℕ} → x ⊔ y ≡ z → x ≤ z
@ -74,18 +75,19 @@ private
            helper : x ⊔ (x ⊓ y) ≤ x ⊔ x  → x ⊔ x ≡ x → x ⊔ (x ⊓ y) ≤ x
            helper x⊔x⊓y≤x⊔x x⊔x≡x rewrite x⊔x≡x = x⊔x⊓y≤x⊔x

-isLattice : IsLattice ℕ _≡_ _⊔_ _⊓_
-isLattice = record
-    { joinSemilattice = isMaxSemilattice
-    ; meetSemilattice = isMinSemilattice
-    ; absorb-⊔-⊓ = λ x y → maxmin-absorb {x} {y}
-    ; absorb-⊓-⊔ = λ x y → minmax-absorb {x} {y}
-    }
+instance
+    isLattice : IsLattice ℕ _≡_ _⊔_ _⊓_
+    isLattice = record
+        { joinSemilattice = isMaxSemilattice
+        ; meetSemilattice = isMinSemilattice
+        ; absorb-⊔-⊓ = λ x y → maxmin-absorb {x} {y}
+        ; absorb-⊓-⊔ = λ x y → minmax-absorb {x} {y}
+        }

-lattice : Lattice ℕ
-lattice = record
-    { _≈_ = _≡_
-    ; _⊔_ = _⊔_
-    ; _⊓_ = _⊓_
-    ; isLattice = isLattice
-    }
+    lattice : Lattice ℕ
+    lattice = record
+        { _≈_ = _≡_
+        ; _⊔_ = _⊔_
+        ; _⊓_ = _⊓_
+        ; isLattice = isLattice
+        }
--- a/Lattice/Prod.agda
+++ b/Lattice/Prod.agda
@ -1,10 +1,10 @@
 open import Lattice

-module Lattice.Prod {a b} {A : Set a} {B : Set b}
-    (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set b)
-    (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B)
-    (_⊓₁_ : A → A → A) (_⊓₂_ : B → B → B)
-    (lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
+module Lattice.Prod {a b} (A : Set a) (B : Set b)
+    {_≈₁_ : A → A → Set a} {_≈₂_ : B → B → Set b}
+    {_⊔₁_ : A → A → A} {_⊔₂_ : B → B → B}
+    {_⊓₁_ : A → A → A} {_⊓₂_ : B → B → B}
+    {{lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_}} {{lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_}} where

 open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
 open import Data.Nat using (ℕ; _≤_; _+_; suc)
@ -12,6 +12,7 @@ open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
 open import Data.Empty using (⊥-elim)
 open import Relation.Binary.Core using (_Preserves_⟶_ )
 open import Relation.Binary.PropositionalEquality using (sym; subst)
+open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Nullary using (¬_; yes; no)
 open import Equivalence
 import Chain
@ -39,13 +40,14 @@ open IsLattice lB using () renaming
 _≈_ : A × B → A × B → Set (a ⊔ℓ b)
 (a₁ , b₁) ≈ (a₂ , b₂) = (a₁ ≈₁ a₂) × (b₁ ≈₂ b₂)

-≈-equiv : IsEquivalence (A × B) _≈_
-≈-equiv = record
-    { ≈-refl = λ {p} → (≈₁-refl , ≈₂-refl)
-    ; ≈-sym = λ {p₁} {p₂} (a₁≈a₂ , b₁≈b₂) → (≈₁-sym a₁≈a₂ , ≈₂-sym b₁≈b₂)
-    ; ≈-trans = λ {p₁} {p₂} {p₃} (a₁≈a₂ , b₁≈b₂) (a₂≈a₃ , b₂≈b₃) →
-        ( ≈₁-trans a₁≈a₂ a₂≈a₃ , ≈₂-trans b₁≈b₂ b₂≈b₃ )
-    }
+instance
+    ≈-equiv : IsEquivalence (A × B) _≈_
+    ≈-equiv = record
+        { ≈-refl = λ {p} → (≈₁-refl , ≈₂-refl)
+        ; ≈-sym = λ {p₁} {p₂} (a₁≈a₂ , b₁≈b₂) → (≈₁-sym a₁≈a₂ , ≈₂-sym b₁≈b₂)
+        ; ≈-trans = λ {p₁} {p₂} {p₃} (a₁≈a₂ , b₁≈b₂) (a₂≈a₃ , b₂≈b₃) →
+            ( ≈₁-trans a₁≈a₂ a₂≈a₃ , ≈₂-trans b₁≈b₂ b₂≈b₃ )
+        }

 _⊔_ : A × B → A × B → A × B
 (a₁ , b₁) ⊔ (a₂ , b₂) = (a₁ ⊔₁ a₂ , b₁ ⊔₂ b₂)
@ -75,116 +77,123 @@ private module ProdIsSemilattice (f₁ : A → A → A) (f₂ : B → B → B) (
            )
        }

-isJoinSemilattice : IsSemilattice (A × B) _≈_ _⊔_
-isJoinSemilattice = ProdIsSemilattice.isSemilattice _⊔₁_ _⊔₂_ joinSemilattice₁ joinSemilattice₂
+instance
+    isJoinSemilattice : IsSemilattice (A × B) _≈_ _⊔_
+    isJoinSemilattice = ProdIsSemilattice.isSemilattice _⊔₁_ _⊔₂_ joinSemilattice₁ joinSemilattice₂

-isMeetSemilattice : IsSemilattice (A × B) _≈_ _⊓_
-isMeetSemilattice = ProdIsSemilattice.isSemilattice _⊓₁_ _⊓₂_ meetSemilattice₁ meetSemilattice₂
+    isMeetSemilattice : IsSemilattice (A × B) _≈_ _⊓_
+    isMeetSemilattice = ProdIsSemilattice.isSemilattice _⊓₁_ _⊓₂_ meetSemilattice₁ meetSemilattice₂

-isLattice : IsLattice (A × B) _≈_ _⊔_ _⊓_
-isLattice = record
-    { joinSemilattice = isJoinSemilattice
-    ; meetSemilattice = isMeetSemilattice
-    ; absorb-⊔-⊓ = λ (a₁ , b₁) (a₂ , b₂) →
-        ( IsLattice.absorb-⊔-⊓ lA a₁ a₂
-        , IsLattice.absorb-⊔-⊓ lB b₁ b₂
-        )
-    ; absorb-⊓-⊔ = λ (a₁ , b₁) (a₂ , b₂) →
-        ( IsLattice.absorb-⊓-⊔ lA a₁ a₂
-        , IsLattice.absorb-⊓-⊔ lB b₁ b₂
-        )
-    }
+    isLattice : IsLattice (A × B) _≈_ _⊔_ _⊓_
+    isLattice = record
+        { joinSemilattice = isJoinSemilattice
+        ; meetSemilattice = isMeetSemilattice
+        ; absorb-⊔-⊓ = λ (a₁ , b₁) (a₂ , b₂) →
+            ( IsLattice.absorb-⊔-⊓ lA a₁ a₂
+            , IsLattice.absorb-⊔-⊓ lB b₁ b₂
+            )
+        ; absorb-⊓-⊔ = λ (a₁ , b₁) (a₂ , b₂) →
+            ( IsLattice.absorb-⊓-⊔ lA a₁ a₂
+            , IsLattice.absorb-⊓-⊔ lB b₁ b₂
+            )
+        }

-lattice : Lattice (A × B)
-lattice = record
-    { _≈_ = _≈_
-    ; _⊔_ = _⊔_
-    ; _⊓_ = _⊓_
-    ; isLattice = isLattice
-    }
+    lattice : Lattice (A × B)
+    lattice = record
+        { _≈_ = _≈_
+        ; _⊔_ = _⊔_
+        ; _⊓_ = _⊓_
+        ; isLattice = isLattice
+        }

-module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_) where
-    ≈-dec : IsDecidable _≈_
+module _ {{≈₁-Decidable : IsDecidable _≈₁_}} {{≈₂-Decidable : IsDecidable _≈₂_}} where
+    open IsDecidable ≈₁-Decidable using () renaming (R-dec to ≈₁-dec)
+    open IsDecidable ≈₂-Decidable using () renaming (R-dec to ≈₂-dec)
+
+    ≈-dec : Decidable _≈_
    ≈-dec (a₁ , b₁) (a₂ , b₂)
        with ≈₁-dec a₁ a₂ | ≈₂-dec b₁ b₂
    ...   | yes a₁≈a₂ | yes b₁≈b₂ = yes (a₁≈a₂ , b₁≈b₂)
    ...   | no a₁̷≈a₂ | _ = no (λ (a₁≈a₂ , _) → a₁̷≈a₂ a₁≈a₂)
    ...   | _ | no b₁̷≈b₂ = no (λ (_ , b₁≈b₂) → b₁̷≈b₂ b₁≈b₂)

+    instance
+        ≈-Decidable : IsDecidable _≈_
+        ≈-Decidable = record { R-dec = ≈-dec }

-module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
-         (h₁ h₂ : ℕ)
-         (fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where
+    module _ {h₁ h₂ : ℕ}
+             {{fhA : FixedHeight₁ h₁}} {{fhB : FixedHeight₂ h₂}} where

-    open import Data.Nat.Properties
-    open IsLattice isLattice using (_≼_; _≺_; ≺-cong)
+        open import Data.Nat.Properties
+        open IsLattice isLattice using (_≼_; _≺_; ≺-cong)

-    module ChainMapping₁ = ChainMapping joinSemilattice₁ isJoinSemilattice
-    module ChainMapping₂ = ChainMapping joinSemilattice₂ isJoinSemilattice
+        module ChainMapping₁ = ChainMapping joinSemilattice₁ isJoinSemilattice
+        module ChainMapping₂ = ChainMapping joinSemilattice₂ isJoinSemilattice

-    module ChainA = Chain _≈₁_ ≈₁-equiv _≺₁_ ≺₁-cong
-    module ChainB = Chain _≈₂_ ≈₂-equiv _≺₂_ ≺₂-cong
-    module ProdChain = Chain _≈_ ≈-equiv _≺_ ≺-cong
+        module ChainA = Chain _≈₁_ ≈₁-equiv _≺₁_ ≺₁-cong
+        module ChainB = Chain _≈₂_ ≈₂-equiv _≺₂_ ≺₂-cong
+        module ProdChain = Chain _≈_ ≈-equiv _≺_ ≺-cong

-    open ChainA using () renaming (Chain to Chain₁; done to done₁; step to step₁; Chain-≈-cong₁ to Chain₁-≈-cong₁)
-    open ChainB using () renaming (Chain to Chain₂; done to done₂; step to step₂; Chain-≈-cong₁ to Chain₂-≈-cong₁)
-    open ProdChain using (Chain; concat; done; step)
+        open ChainA using () renaming (Chain to Chain₁; done to done₁; step to step₁; Chain-≈-cong₁ to Chain₁-≈-cong₁)
+        open ChainB using () renaming (Chain to Chain₂; done to done₂; step to step₂; Chain-≈-cong₁ to Chain₂-≈-cong₁)
+        open ProdChain using (Chain; concat; done; step)

-    private
-        a,∙-Monotonic : ∀ (a : A) → Monotonic _≼₂_ _≼_ (λ b → (a , b))
-        a,∙-Monotonic a {b₁} {b₂} b₁⊔b₂≈b₂ = (⊔₁-idemp a , b₁⊔b₂≈b₂)
+        private
+            a,∙-Monotonic : ∀ (a : A) → Monotonic _≼₂_ _≼_ (λ b → (a , b))
+            a,∙-Monotonic a {b₁} {b₂} b₁⊔b₂≈b₂ = (⊔₁-idemp a , b₁⊔b₂≈b₂)

-        a,∙-Preserves-≈₂ : ∀ (a : A) → (λ b → (a , b)) Preserves _≈₂_ ⟶  _≈_
-        a,∙-Preserves-≈₂ a {b₁} {b₂} b₁≈b₂ = (≈₁-refl , b₁≈b₂)
+            a,∙-Preserves-≈₂ : ∀ (a : A) → (λ b → (a , b)) Preserves _≈₂_ ⟶  _≈_
+            a,∙-Preserves-≈₂ a {b₁} {b₂} b₁≈b₂ = (≈₁-refl , b₁≈b₂)

-        ∙,b-Monotonic : ∀ (b : B) → Monotonic _≼₁_ _≼_ (λ a → (a , b))
-        ∙,b-Monotonic b {a₁} {a₂} a₁⊔a₂≈a₂ = (a₁⊔a₂≈a₂ , ⊔₂-idemp b)
+            ∙,b-Monotonic : ∀ (b : B) → Monotonic _≼₁_ _≼_ (λ a → (a , b))
+            ∙,b-Monotonic b {a₁} {a₂} a₁⊔a₂≈a₂ = (a₁⊔a₂≈a₂ , ⊔₂-idemp b)

-        ∙,b-Preserves-≈₁ : ∀ (b : B) → (λ a → (a , b)) Preserves _≈₁_ ⟶  _≈_
-        ∙,b-Preserves-≈₁ b {a₁} {a₂} a₁≈a₂ = (a₁≈a₂ , ≈₂-refl)
+            ∙,b-Preserves-≈₁ : ∀ (b : B) → (λ a → (a , b)) Preserves _≈₁_ ⟶  _≈_
+            ∙,b-Preserves-≈₁ b {a₁} {a₂} a₁≈a₂ = (a₁≈a₂ , ≈₂-refl)

-        open ChainA.Height fhA using () renaming (⊥ to ⊥₁; ⊤ to ⊤₁; longestChain to longestChain₁; bounded to bounded₁)
-        open ChainB.Height fhB using () renaming (⊥ to ⊥₂; ⊤ to ⊤₂; longestChain to longestChain₂; bounded to bounded₂)
+            open ChainA.Height fhA using () renaming (⊥ to ⊥₁; ⊤ to ⊤₁; longestChain to longestChain₁; bounded to bounded₁)
+            open ChainB.Height fhB using () renaming (⊥ to ⊥₂; ⊤ to ⊤₂; longestChain to longestChain₂; bounded to bounded₂)

-        unzip : ∀ {a₁ a₂ : A} {b₁ b₂ : B} {n : ℕ} → Chain (a₁ , b₁) (a₂ , b₂) n → Σ (ℕ × ℕ) (λ (n₁ , n₂) → ((Chain₁ a₁ a₂ n₁ × Chain₂ b₁ b₂ n₂) × (n ≤ n₁ + n₂)))
-        unzip (done (a₁≈a₂ , b₁≈b₂)) = ((0 , 0) , ((done₁ a₁≈a₂ , done₂ b₁≈b₂) , ≤-refl))
-        unzip {a₁} {a₂} {b₁} {b₂} {n} (step {(a₁ , b₁)} {(a , b)} ((a₁≼a , b₁≼b) , a₁b₁̷≈ab) (a≈a' , b≈b') a'b'a₂b₂)
-            with ≈₁-dec a₁ a | ≈₂-dec b₁ b | unzip a'b'a₂b₂
-        ...   | yes a₁≈a | yes b₁≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) = ⊥-elim (a₁b₁̷≈ab (a₁≈a , b₁≈b))
-        ...   | no a₁̷≈a  | yes b₁≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) =
-                ((suc n₁ , n₂) , ((step₁ (a₁≼a , a₁̷≈a) a≈a' c₁ , Chain₂-≈-cong₁ (≈₂-sym (≈₂-trans b₁≈b b≈b')) c₂), +-monoʳ-≤ 1 (n≤n₁+n₂)))
-        ...   | yes a₁≈a | no b₁̷≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) =
-                ((n₁ , suc n₂) , ( (Chain₁-≈-cong₁ (≈₁-sym (≈₁-trans a₁≈a a≈a')) c₁ , step₂ (b₁≼b , b₁̷≈b) b≈b' c₂)
-                                 , subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂)
-                                 ))
-        ...   | no a₁̷≈a  | no b₁̷≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) =
-                ((suc n₁ , suc n₂) , ( (step₁ (a₁≼a , a₁̷≈a) a≈a' c₁ , step₂ (b₁≼b , b₁̷≈b) b≈b' c₂)
-                                     , m≤n⇒m≤o+n 1 (subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂))
+            unzip : ∀ {a₁ a₂ : A} {b₁ b₂ : B} {n : ℕ} → Chain (a₁ , b₁) (a₂ , b₂) n → Σ (ℕ × ℕ) (λ (n₁ , n₂) → ((Chain₁ a₁ a₂ n₁ × Chain₂ b₁ b₂ n₂) × (n ≤ n₁ + n₂)))
+            unzip (done (a₁≈a₂ , b₁≈b₂)) = ((0 , 0) , ((done₁ a₁≈a₂ , done₂ b₁≈b₂) , ≤-refl))
+            unzip {a₁} {a₂} {b₁} {b₂} {n} (step {(a₁ , b₁)} {(a , b)} ((a₁≼a , b₁≼b) , a₁b₁̷≈ab) (a≈a' , b≈b') a'b'a₂b₂)
+                with ≈₁-dec a₁ a | ≈₂-dec b₁ b | unzip a'b'a₂b₂
+            ...   | yes a₁≈a | yes b₁≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) = ⊥-elim (a₁b₁̷≈ab (a₁≈a , b₁≈b))
+            ...   | no a₁̷≈a  | yes b₁≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) =
+                    ((suc n₁ , n₂) , ((step₁ (a₁≼a , a₁̷≈a) a≈a' c₁ , Chain₂-≈-cong₁ (≈₂-sym (≈₂-trans b₁≈b b≈b')) c₂), +-monoʳ-≤ 1 (n≤n₁+n₂)))
+            ...   | yes a₁≈a | no b₁̷≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) =
+                    ((n₁ , suc n₂) , ( (Chain₁-≈-cong₁ (≈₁-sym (≈₁-trans a₁≈a a≈a')) c₁ , step₂ (b₁≼b , b₁̷≈b) b≈b' c₂)
+                                     , subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂)
                                     ))
+            ...   | no a₁̷≈a  | no b₁̷≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) =
+                    ((suc n₁ , suc n₂) , ( (step₁ (a₁≼a , a₁̷≈a) a≈a' c₁ , step₂ (b₁≼b , b₁̷≈b) b≈b' c₂)
+                                         , m≤n⇒m≤o+n 1 (subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂))
+                                         ))

-    fixedHeight : IsLattice.FixedHeight isLattice (h₁ + h₂)
-    fixedHeight = record
-      { ⊥ = (⊥₁ , ⊥₂)
-      ; ⊤ = (⊤₁ , ⊤₂)
-      ; longestChain = concat
-            (ChainMapping₁.Chain-map (λ a → (a , ⊥₂)) (∙,b-Monotonic _) proj₁ (∙,b-Preserves-≈₁ _) longestChain₁)
-            (ChainMapping₂.Chain-map (λ b → (⊤₁ , b)) (a,∙-Monotonic _) proj₂ (a,∙-Preserves-≈₂ _) longestChain₂)
-      ; bounded = λ a₁b₁a₂b₂ →
-            let ((n₁ , n₂) , ((a₁a₂ , b₁b₂) , n≤n₁+n₂)) = unzip a₁b₁a₂b₂
-            in ≤-trans n≤n₁+n₂ (+-mono-≤ (bounded₁ a₁a₂) (bounded₂ b₁b₂))
-      }
+        instance
+            fixedHeight : IsLattice.FixedHeight isLattice (h₁ + h₂)
+            fixedHeight = record
+              { ⊥ = (⊥₁ , ⊥₂)
+              ; ⊤ = (⊤₁ , ⊤₂)
+              ; longestChain = concat
+                    (ChainMapping₁.Chain-map (λ a → (a , ⊥₂)) (∙,b-Monotonic _) proj₁ (∙,b-Preserves-≈₁ _) longestChain₁)
+                    (ChainMapping₂.Chain-map (λ b → (⊤₁ , b)) (a,∙-Monotonic _) proj₂ (a,∙-Preserves-≈₂ _) longestChain₂)
+              ; bounded = λ a₁b₁a₂b₂ →
+                    let ((n₁ , n₂) , ((a₁a₂ , b₁b₂) , n≤n₁+n₂)) = unzip a₁b₁a₂b₂
+                    in ≤-trans n≤n₁+n₂ (+-mono-≤ (bounded₁ a₁a₂) (bounded₂ b₁b₂))
+              }

-    isFiniteHeightLattice : IsFiniteHeightLattice (A × B) (h₁ + h₂) _≈_ _⊔_ _⊓_
-    isFiniteHeightLattice = record
-        { isLattice = isLattice
-        ; fixedHeight = fixedHeight
-        }
+            isFiniteHeightLattice : IsFiniteHeightLattice (A × B) (h₁ + h₂) _≈_ _⊔_ _⊓_
+            isFiniteHeightLattice = record
+                { isLattice = isLattice
+                ; fixedHeight = fixedHeight
+                }

-    finiteHeightLattice : FiniteHeightLattice (A × B)
-    finiteHeightLattice = record
-        { height = h₁ + h₂
-        ; _≈_ = _≈_
-        ; _⊔_ = _⊔_
-        ; _⊓_ = _⊓_
-        ; isFiniteHeightLattice = isFiniteHeightLattice
-        }
+            finiteHeightLattice : FiniteHeightLattice (A × B)
+            finiteHeightLattice = record
+                { height = h₁ + h₂
+                ; _≈_ = _≈_
+                ; _⊔_ = _⊔_
+                ; _⊓_ = _⊓_
+                ; isFiniteHeightLattice = isFiniteHeightLattice
+                }
--- a/Lattice/Unit.agda
+++ b/Lattice/Unit.agda
@ -7,6 +7,7 @@ open import Data.Unit using (⊤; tt) public
 open import Data.Unit.Properties using (_≟_; ≡-setoid)
 open import Relation.Binary using (Setoid)
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_)
+open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Nullary using (Dec; ¬_; yes; no)
 open import Equivalence
 open import Lattice
@ -24,9 +25,13 @@ _≈_ = _≡_
    ; ≈-trans = trans
    }

-≈-dec : IsDecidable _≈_
+≈-dec : Decidable _≈_
 ≈-dec = _≟_

+instance
+    ≈-Decidable : IsDecidable _≈_
+    ≈-Decidable = record { R-dec = ≈-dec }
+
 _⊔_ : ⊤ → ⊤ → ⊤
 tt ⊔ tt = tt

@ -45,14 +50,15 @@ tt ⊓ tt = tt
 ⊔-idemp : (x : ⊤) → (x ⊔ x) ≈ x
 ⊔-idemp tt = Eq.refl

-isJoinSemilattice : IsSemilattice ⊤ _≈_ _⊔_
-isJoinSemilattice = record
-    { ≈-equiv = ≈-equiv
-    ; ≈-⊔-cong = ≈-⊔-cong
-    ; ⊔-assoc = ⊔-assoc
-    ; ⊔-comm  = ⊔-comm
-    ; ⊔-idemp = ⊔-idemp
-    }
+instance
+    isJoinSemilattice : IsSemilattice ⊤ _≈_ _⊔_
+    isJoinSemilattice = record
+        { ≈-equiv = ≈-equiv
+        ; ≈-⊔-cong = ≈-⊔-cong
+        ; ⊔-assoc = ⊔-assoc
+        ; ⊔-comm  = ⊔-comm
+        ; ⊔-idemp = ⊔-idemp
+        }

 ≈-⊓-cong : ∀ {ab₁ ab₂ ab₃ ab₄} → ab₁ ≈ ab₂ → ab₃ ≈ ab₄ → (ab₁ ⊓ ab₃) ≈ (ab₂ ⊓ ab₄)
 ≈-⊓-cong {tt} {tt} {tt} {tt} _ _ = Eq.refl
@ -66,36 +72,32 @@ isJoinSemilattice = record
 ⊓-idemp : (x : ⊤) → (x ⊓ x) ≈ x
 ⊓-idemp tt = Eq.refl

-isMeetSemilattice : IsSemilattice ⊤ _≈_ _⊓_
-isMeetSemilattice = record
-    { ≈-equiv = ≈-equiv
-    ; ≈-⊔-cong = ≈-⊓-cong
-    ; ⊔-assoc = ⊓-assoc
-    ; ⊔-comm  = ⊓-comm
-    ; ⊔-idemp = ⊓-idemp
-    }
+instance
+    isMeetSemilattice : IsSemilattice ⊤ _≈_ _⊓_
+    isMeetSemilattice = record
+        { ≈-equiv = ≈-equiv
+        ; ≈-⊔-cong = ≈-⊓-cong
+        ; ⊔-assoc = ⊓-assoc
+        ; ⊔-comm  = ⊓-comm
+        ; ⊔-idemp = ⊓-idemp
+        }

-absorb-⊔-⊓ : (x y : ⊤) → (x ⊔ (x ⊓ y)) ≈ x
-absorb-⊔-⊓ tt tt = Eq.refl
+instance
+    isLattice : IsLattice ⊤ _≈_ _⊔_ _⊓_
+    isLattice = record
+        { joinSemilattice = isJoinSemilattice
+        ; meetSemilattice = isMeetSemilattice
+        ; absorb-⊔-⊓ = λ { tt tt → Eq.refl }
+        ; absorb-⊓-⊔ = λ { tt tt → Eq.refl }
+        }

-absorb-⊓-⊔ : (x y : ⊤) → (x ⊓ (x ⊔ y)) ≈ x
-absorb-⊓-⊔ tt tt = Eq.refl
-
-isLattice : IsLattice ⊤ _≈_ _⊔_ _⊓_
-isLattice = record
-    { joinSemilattice = isJoinSemilattice
-    ; meetSemilattice = isMeetSemilattice
-    ; absorb-⊔-⊓ = absorb-⊔-⊓
-    ; absorb-⊓-⊔ = absorb-⊓-⊔
-    }
-
-lattice : Lattice ⊤
-lattice = record
-    { _≈_ = _≈_
-    ; _⊔_ = _⊔_
-    ; _⊓_ = _⊓_
-    ; isLattice = isLattice
-    }
+    lattice : Lattice ⊤
+    lattice = record
+        { _≈_ = _≈_
+        ; _⊔_ = _⊔_
+        ; _⊓_ = _⊓_
+        ; isLattice = isLattice
+        }

 open Chain _≈_ ≈-equiv (IsLattice._≺_ isLattice) (IsLattice.≺-cong isLattice)

@ -107,25 +109,26 @@ private
    isLongest {tt} {tt} (step (tt⊔tt≈tt , tt̷≈tt) _ _) = ⊥-elim (tt̷≈tt refl)
    isLongest (done _) = z≤n

-fixedHeight : IsLattice.FixedHeight isLattice 0
-fixedHeight = record
-    { ⊥ = tt
-    ; ⊤ = tt
-    ; longestChain = longestChain
-    ; bounded = isLongest
-    }
+instance
+    fixedHeight : IsLattice.FixedHeight isLattice 0
+    fixedHeight = record
+        { ⊥ = tt
+        ; ⊤ = tt
+        ; longestChain = longestChain
+        ; bounded = isLongest
+        }

-isFiniteHeightLattice : IsFiniteHeightLattice ⊤ 0 _≈_ _⊔_ _⊓_
-isFiniteHeightLattice = record
-    { isLattice = isLattice
-    ; fixedHeight = fixedHeight
-    }
+    isFiniteHeightLattice : IsFiniteHeightLattice ⊤ 0 _≈_ _⊔_ _⊓_
+    isFiniteHeightLattice = record
+        { isLattice = isLattice
+        ; fixedHeight = fixedHeight
+        }

-finiteHeightLattice : FiniteHeightLattice ⊤
-finiteHeightLattice = record
-    { height = 0
-    ; _≈_ = _≈_
-    ; _⊔_ = _⊔_
-    ; _⊓_ = _⊓_
-    ; isFiniteHeightLattice = isFiniteHeightLattice
-    }
+    finiteHeightLattice : FiniteHeightLattice ⊤
+    finiteHeightLattice = record
+        { height = 0
+        ; _≈_ = _≈_
+        ; _⊔_ = _⊔_
+        ; _⊓_ = _⊓_
+        ; isFiniteHeightLattice = isFiniteHeightLattice
+        }
--- 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
Author	SHA1	Message	Date
Danila Fedorin	cf824dc744	Switch product to using instances Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-01-04 21:33:59 -08:00
Danila Fedorin	70847d51db	Swich AboveBelow to using instances Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-01-04 21:23:07 -08:00
Danila Fedorin	d96eb97b69	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
Danila Fedorin	d90b544436	Use binary operator for decidable equality consistently Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-01-04 19:08:28 -08:00
Danila Fedorin	b0488c9cc6	Make 'IsDecidable' into a record to aid instance search Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-01-04 18:58:56 -08:00
Danila Fedorin	8abf6f8670	Make 'isLattice' for simple types be an instance Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-01-04 17:27:38 -08:00