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,20 +63,22 @@ 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
+
+    instance
+        fixedHeight = record
            { ⊥ = f ⊥₁
            ; ⊤ = f ⊤₁
            ; longestChain = portChain₁ c
            ; bounded = λ c' → bounded₁ (portChain₂ c')
            }
+
+        isFiniteHeightLattice : IsFiniteHeightLattice B height _≈₂_ _⊔₂_ _⊓₂_
+        isFiniteHeightLattice = record
+            { isLattice = lB
+            ; fixedHeight = fixedHeight
            }

        finiteHeightLattice : FiniteHeightLattice B
--- 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,6 +177,7 @@ module Plain (x : A) where
    ⊔-idemp ⊥ = ≈-⊥-⊥
    ⊔-idemp [ x ] rewrite x≈y⇒[x]⊔[y]≡[x] (≈₁-refl {x}) = ≈-refl

+    instance
        isJoinSemilattice : IsSemilattice AboveBelow _≈_ _⊔_
        isJoinSemilattice = record
            { ≈-equiv = ≈-equiv
@ -262,6 +271,7 @@ module Plain (x : A) where
    ⊓-idemp ⊤ = ≈-⊤-⊤
    ⊓-idemp [ x ] rewrite x≈y⇒[x]⊓[y]≡[x] (≈₁-refl {x}) = ≈-refl

+    instance
        isMeetSemilattice : IsSemilattice AboveBelow _≈_ _⊓_
        isMeetSemilattice = record
            { ≈-equiv = ≈-equiv
@ -294,6 +304,7 @@ module Plain (x : A) where
    ...   | no x̷≈y rewrite x̷≈y⇒[x]⊔[y]≡⊤ x̷≈y rewrite x⊓⊤≡x [ x ] = ≈-refl


+    instance
        isLattice : IsLattice AboveBelow _≈_ _⊔_ _⊓_
        isLattice = record
            { joinSemilattice = isJoinSemilattice
@ -354,6 +365,7 @@ 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)

+    instance
        fixedHeight : IsLattice.FixedHeight isLattice 2
        fixedHeight = record
            { ⊥ = ⊥
--- 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,6 +144,7 @@ module WithKeys (ks : List A) where
                IsEquivalence.≈-trans ≈ᵐ-equiv {m₁} {m₂} {m₃}
        }

+    instance
        isUnionSemilattice : IsSemilattice FiniteMap _≈_ _⊔_
        isUnionSemilattice = record
            { ≈-equiv = ≈-equiv
@ -170,8 +175,6 @@ module WithKeys (ks : List A) where
            ; absorb-⊓-⊔ = λ (m₁ , _) (m₂ , _) → absorb-⊓ᵐ-⊔ᵐ m₁ m₂
            }

-    open IsLattice isLattice using (_≼_; ⊔-Monotonicˡ; ⊔-Monotonicʳ) public
-
        lattice : Lattice FiniteMap
        lattice = record
            { _≈_ = _≈_
@ -180,6 +183,8 @@ module WithKeys (ks : List A) where
            ; isLattice = isLattice
            }

+    open IsLattice isLattice using (_≼_; ⊔-Monotonicˡ; ⊔-Monotonicʳ) public
+
    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,16 +112,14 @@ 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
@ -131,22 +129,25 @@ module _ (k : ℕ) where
            ; isLattice = isLattice
            }

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

        private
-            required : RequiredForFixedHeight
-            required = record
-                { ≈₁-dec = ≈₁-dec
-                ; ≈₂-dec = ≈₂-dec
+            isFiniteHeightWithBotAndDecEq =
+                Everything.isFiniteHeightIfSupported (everything k)
+                    record
+                        { ≈₁-Decidable = ≈₁-Decidable
+                        ; ≈₂-Decidable = ≈₂-Decidable
                        ; h₁ = h₁
                        ; h₂ = h₂
                        ; fhA = fhA
                        ; fhB = fhB
                        }
+        open IsFiniteHeightWithBotAndDecEq isFiniteHeightWithBotAndDecEq using (height; ⊥-correct)

-        fixedHeight = IsFiniteHeightWithBotAndDecEq.fixedHeight (Everything.isFiniteHeightIfSupported (everything k) required)
+        instance
+            fixedHeight = IsFiniteHeightWithBotAndDecEq.fixedHeight isFiniteHeightWithBotAndDecEq

            isFiniteHeightLattice = record
                { isLattice = isLattice
@ -155,7 +156,7 @@ module _ (k : ℕ) where

            finiteHeightLattice : FiniteHeightLattice (IterProd k)
            finiteHeightLattice = record
-            { height = IsFiniteHeightWithBotAndDecEq.height (Everything.isFiniteHeightIfSupported (everything k) required)
+                { height = height
                ; _≈_ = _≈_
                ; _⊔_ = _⊔_
                ; _⊓_ = _⊓_
@ -163,5 +164,5 @@ module _ (k : ℕ) where
                }

        ⊥-built : Height.⊥ fixedHeight ≡ (build (Height.⊥ fhA) (Height.⊥ fhB) k)
-        ⊥-built = IsFiniteHeightWithBotAndDecEq.⊥-correct (Everything.isFiniteHeightIfSupported (everything k) required)
+        ⊥-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,8 +18,9 @@ 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
+instance
+    isMaxSemilattice : IsSemilattice ℕ _≡_ _⊔_
+    isMaxSemilattice = record
        { ≈-equiv = record
            { ≈-refl = refl
            ; ≈-sym = sym
@ -31,8 +32,8 @@ isMaxSemilattice = record
        ; ⊔-idemp = ⊔-idem
        }

-isMinSemilattice : IsSemilattice ℕ _≡_ _⊓_
-isMinSemilattice = record
+    isMinSemilattice : IsSemilattice ℕ _≡_ _⊓_
+    isMinSemilattice = record
        { ≈-equiv = record
            { ≈-refl = refl
            ; ≈-sym = sym
@ -74,16 +75,17 @@ 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
+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
+    lattice : Lattice ℕ
+    lattice = record
        { _≈_ = _≡_
        ; _⊔_ = _⊔_
        ; _⊓_ = _⊓_
--- 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,8 +40,9 @@ 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
+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₃) →
@ -75,14 +77,15 @@ 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
+    isLattice : IsLattice (A × B) _≈_ _⊔_ _⊓_
+    isLattice = record
        { joinSemilattice = isJoinSemilattice
        ; meetSemilattice = isMeetSemilattice
        ; absorb-⊔-⊓ = λ (a₁ , b₁) (a₂ , b₂) →
@ -95,26 +98,31 @@ isLattice = record
            )
        }

-lattice : Lattice (A × B)
-lattice = record
+    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)
@ -162,6 +170,7 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
                                         , m≤n⇒m≤o+n 1 (subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂))
                                         ))

+        instance
            fixedHeight : IsLattice.FixedHeight isLattice (h₁ + h₂)
            fixedHeight = record
              { ⊥ = (⊥₁ , ⊥₂)
--- 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,8 +50,9 @@ tt ⊓ tt = tt
 ⊔-idemp : (x : ⊤) → (x ⊔ x) ≈ x
 ⊔-idemp tt = Eq.refl

-isJoinSemilattice : IsSemilattice ⊤ _≈_ _⊔_
-isJoinSemilattice = record
+instance
+    isJoinSemilattice : IsSemilattice ⊤ _≈_ _⊔_
+    isJoinSemilattice = record
        { ≈-equiv = ≈-equiv
        ; ≈-⊔-cong = ≈-⊔-cong
        ; ⊔-assoc = ⊔-assoc
@ -66,8 +72,9 @@ isJoinSemilattice = record
 ⊓-idemp : (x : ⊤) → (x ⊓ x) ≈ x
 ⊓-idemp tt = Eq.refl

-isMeetSemilattice : IsSemilattice ⊤ _≈_ _⊓_
-isMeetSemilattice = record
+instance
+    isMeetSemilattice : IsSemilattice ⊤ _≈_ _⊓_
+    isMeetSemilattice = record
        { ≈-equiv = ≈-equiv
        ; ≈-⊔-cong = ≈-⊓-cong
        ; ⊔-assoc = ⊓-assoc
@ -75,22 +82,17 @@ isMeetSemilattice = record
        ; ⊔-idemp = ⊓-idemp
        }

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

-lattice : Lattice ⊤
-lattice = record
+    lattice : Lattice ⊤
+    lattice = record
        { _≈_ = _≈_
        ; _⊔_ = _⊔_
        ; _⊓_ = _⊓_
@ -107,22 +109,23 @@ 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
+instance
+    fixedHeight : IsLattice.FixedHeight isLattice 0
+    fixedHeight = record
        { ⊥ = tt
        ; ⊤ = tt
        ; longestChain = longestChain
        ; bounded = isLongest
        }

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

-finiteHeightLattice : FiniteHeightLattice ⊤
-finiteHeightLattice = record
+    finiteHeightLattice : FiniteHeightLattice ⊤
+    finiteHeightLattice = record
        { height = 0
        ; _≈_ = _≈_
        ; _⊔_ = _⊔_
--- 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