More cleanup to FiniteValueMap

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

Lattice/AboveBelow.agda

@@ -10,10 +10,14 @@ module Lattice.AboveBelow {a} (A : Set a)
 open import Data.Empty using (⊥-elim)
 open import Data.Product using (_,_)
 open import Data.Nat using (_≤_; ℕ; z≤n; s≤s; suc)
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; subst; refl)
+open import Function using (_∘_)
+open import Relation.Binary.PropositionalEquality as Eq
+    using (_≡_; sym; subst; refl)
+
 import Chain
 
-open IsEquivalence ≈₁-equiv using () renaming (≈-refl to ≈₁-refl; ≈-sym to ≈₁-sym; ≈-trans to ≈₁-trans)
+open IsEquivalence ≈₁-equiv using ()
+    renaming (≈-refl to ≈₁-refl; ≈-sym to ≈₁-sym; ≈-trans to ≈₁-trans)
 
 data AboveBelow : Set a where
     ⊥ : AboveBelow
@@ -61,6 +65,9 @@ data _≈_ : AboveBelow → AboveBelow → Set a where
 ≈-dec [ x ] ⊥ = no λ ()
 ≈-dec [ x ] ⊤ = no λ ()
 
+-- 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.
 module Plain where
     _⊔_ : AboveBelow → AboveBelow → AboveBelow
     ⊥ ⊔ x = x
@@ -99,7 +106,8 @@ module Plain where
     ...   | yes x≈₁y = ⊥-elim (x̷≈₁y x≈₁y)
     ...   | no x̷≈₁y = refl
 
-    ≈-⊔-cong : ∀ {ab₁ ab₂ ab₃ ab₄} → ab₁ ≈ ab₂ → ab₃ ≈ ab₄ → (ab₁ ⊔ ab₃) ≈ (ab₂ ⊔ ab₄)
+    ≈-⊔-cong : ∀ {ab₁ ab₂ ab₃ ab₄} → ab₁ ≈ ab₂ → ab₃ ≈ ab₄ →
+               (ab₁ ⊔ ab₃) ≈ (ab₂ ⊔ ab₄)
     ≈-⊔-cong ≈-⊤-⊤ ≈-⊤-⊤ = ≈-⊤-⊤
     ≈-⊔-cong ≈-⊤-⊤ ≈-⊥-⊥ = ≈-⊤-⊤
     ≈-⊔-cong ≈-⊥-⊥ ≈-⊤-⊤ = ≈-⊤-⊤
@@ -115,7 +123,8 @@ module Plain where
     ...   | no  a₁̷≈a₃     | yes a₂≈a₄ = ⊥-elim (a₁̷≈a₃ (≈₁-trans a₁≈a₂ (≈₁-trans a₂≈a₄ (≈₁-sym a₃≈a₄))))
     ...   | no  _         | no  _     = ≈-⊤-⊤
 
-    ⊔-assoc : ∀ (ab₁ ab₂ ab₃ : AboveBelow) → ((ab₁ ⊔ ab₂) ⊔ ab₃) ≈ (ab₁ ⊔ (ab₂ ⊔ ab₃))
+    ⊔-assoc : ∀ (ab₁ ab₂ ab₃ : AboveBelow) →
+              ((ab₁ ⊔ ab₂) ⊔ ab₃) ≈ (ab₁ ⊔ (ab₂ ⊔ ab₃))
     ⊔-assoc ⊤ ab₂ ab₃ = ≈-⊤-⊤
     ⊔-assoc ⊥ ab₂ ab₃ = ≈-refl
     ⊔-assoc [ x₁ ] ⊤ ab₃ = ≈-⊤-⊤
@@ -126,7 +135,7 @@ module Plain where
         with ≈₁-dec x₂ x₃ | ≈₁-dec x₁ x₂
     ...   | no  x₂̷≈x₃ | no _      rewrite x̷≈y⇒[x]⊔[y]≡⊤ x₂̷≈x₃ = ≈-⊤-⊤
     ...   | no  x₂̷≈x₃ | yes x₁≈x₂ rewrite x̷≈y⇒[x]⊔[y]≡⊤ x₂̷≈x₃
-                                  rewrite x̷≈y⇒[x]⊔[y]≡⊤ λ x₁≈x₃ → x₂̷≈x₃ (≈₁-trans (≈₁-sym x₁≈x₂) x₁≈x₃) = ≈-⊤-⊤
+                                  rewrite x̷≈y⇒[x]⊔[y]≡⊤ (x₂̷≈x₃ ∘ (≈₁-trans (≈₁-sym x₁≈x₂))) = ≈-⊤-⊤
     ...   | yes x₂≈x₃ | yes x₁≈x₂ rewrite x≈y⇒[x]⊔[y]≡[x] x₂≈x₃
                                   rewrite x≈y⇒[x]⊔[y]≡[x] x₁≈x₂
                                   rewrite x≈y⇒[x]⊔[y]≡[x] (≈₁-trans x₁≈x₂ x₂≈x₃) = ≈-refl
@@ -139,7 +148,7 @@ module Plain where
     ⊔-comm x ⊥ rewrite x⊔⊥≡x x = ≈-refl
     ⊔-comm [ x₁ ] [ x₂ ] with ≈₁-dec x₁ x₂
     ... | yes x₁≈x₂ rewrite x≈y⇒[x]⊔[y]≡[x] (≈₁-sym x₁≈x₂) = ≈-lift x₁≈x₂
-    ... | no  x₁̷≈x₂ rewrite x̷≈y⇒[x]⊔[y]≡⊤ λ x₂≈x₁ → (x₁̷≈x₂ (≈₁-sym x₂≈x₁)) = ≈-⊤-⊤
+    ... | no  x₁̷≈x₂ rewrite x̷≈y⇒[x]⊔[y]≡⊤ (x₁̷≈x₂ ∘ ≈₁-sym) = ≈-⊤-⊤
 
     ⊔-idemp : ∀ ab → (ab ⊔ ab) ≈ ab
     ⊔-idemp ⊤ = ≈-⊤-⊤

Lattice/FiniteMap.agda

@@ -1,13 +1,13 @@
 open import Lattice
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst)
+open import Relation.Binary.PropositionalEquality as Eq
-open import Relation.Binary.Definitions using (Decidable)
+    using (_≡_;refl; sym; trans; cong; subst)
 open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
 open import Data.List using (List)
 
 module Lattice.FiniteMap {a b : Level} (A : Set a) (B : Set b)
     (_≈₂_ : B → B → Set b)
     (_⊔₂_ : B → B → B) (_⊓₂_ : B → B → B)
-    (≡-dec-A : Decidable (_≡_ {a} {A}))
+    (≡-dec-A : IsDecidable (_≡_ {a} {A}))
     (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
 
 open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB as Map
@@ -43,22 +43,36 @@ module _ (ks : List A) where
     ≈-dec ≈₂-dec fm₁ fm₂ = ≈ᵐ-dec ≈₂-dec (proj₁ fm₁) (proj₁ fm₂)
 
     _⊔_ : FiniteMap → FiniteMap → FiniteMap
-    _⊔_ (m₁ , km₁≡ks) (m₂ , km₂≡ks) = (m₁ ⊔ᵐ m₂ , trans (sym (⊔-equal-keys {m₁} {m₂} (trans (km₁≡ks) (sym km₂≡ks)))) km₁≡ks)
+    _⊔_ (m₁ , km₁≡ks) (m₂ , km₂≡ks) =
+        ( m₁ ⊔ᵐ m₂
+        , trans (sym (⊔-equal-keys {m₁} {m₂} (trans (km₁≡ks) (sym km₂≡ks))))
+                km₁≡ks
+        )
 
     _⊓_ : FiniteMap → FiniteMap → FiniteMap
-    _⊓_ (m₁ , km₁≡ks) (m₂ , km₂≡ks) = (m₁ ⊓ᵐ m₂ , trans (sym (⊓-equal-keys {m₁} {m₂} (trans (km₁≡ks) (sym km₂≡ks)))) km₁≡ks)
+    _⊓_ (m₁ , km₁≡ks) (m₂ , km₂≡ks) =
+        ( m₁ ⊓ᵐ m₂
+        , trans (sym (⊓-equal-keys {m₁} {m₂} (trans (km₁≡ks) (sym km₂≡ks))))
+                km₁≡ks
+        )
 
     ≈-equiv : IsEquivalence FiniteMap _≈_
     ≈-equiv = record
-        { ≈-refl = λ {(m , _)} → IsEquivalence.≈-refl ≈ᵐ-equiv {m}
+        { ≈-refl =
-        ; ≈-sym = λ {(m₁ , _)} {(m₂ , _)} → IsEquivalence.≈-sym ≈ᵐ-equiv {m₁} {m₂}
+            λ {(m , _)} → IsEquivalence.≈-refl ≈ᵐ-equiv {m}
-        ; ≈-trans = λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} → IsEquivalence.≈-trans ≈ᵐ-equiv {m₁} {m₂} {m₃}
+        ; ≈-sym =
+            λ {(m₁ , _)} {(m₂ , _)} → IsEquivalence.≈-sym ≈ᵐ-equiv {m₁} {m₂}
+        ; ≈-trans =
+            λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} →
+                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₄
+        ; ≈-⊔-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
@@ -67,7 +81,9 @@ module _ (ks : List A) where
     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₄
+        ; ≈-⊔-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

Lattice/FiniteValueMap.agda

@@ -4,7 +4,8 @@
 
 open import Lattice
 open import Equivalence
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst)
+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 Function.Definitions using (Inverseˡ; Inverseʳ)
@@ -27,18 +28,45 @@ open import Data.List.Relation.Unary.All using (All)
 open import Data.List.Relation.Unary.Any using (Any; here; there)
 open import Relation.Nullary using (¬_)
 
-open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB using (subset-impl; locate; forget; _∈_; Map-functional; Expr-Provenance; _∩_; _∪_; `_; in₁; in₂; bothᵘ; single; ⊔-combines)
+open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB
+    using
+        ( subset-impl
+        ; locate; forget
+        ; _∈_
+        ; Map-functional
+        ; Expr-Provenance
+        ; _∩_; _∪_; `_
+        ; in₁; in₂; bothᵘ; single
+        ; ⊔-combines
+        )
 open import Lattice.FiniteMap A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB public
 
 module IterProdIsomorphism where
     open import Data.Unit using (⊤; tt)
-    open import Lattice.Unit using () renaming (_≈_ to _≈ᵘ_; _⊔_ to _⊔ᵘ_; _⊓_ to _⊓ᵘ_; ≈-dec to ≈ᵘ-dec; isLattice to isLatticeᵘ; ≈-equiv to ≈ᵘ-equiv; fixedHeight to fixedHeightᵘ)
+    open import Lattice.Unit using ()
-    open import Lattice.IterProd _≈₂_ _≈ᵘ_ _⊔₂_ _⊔ᵘ_ _⊓₂_ _⊓ᵘ_ lB isLatticeᵘ as IP using (IterProd)
+        renaming
-    open IsLattice lB using () renaming (≈-trans to ≈₂-trans; ≈-sym to ≈₂-sym; FixedHeight to FixedHeight₂)
+            ( _≈_ to _≈ᵘ_
+            ; _⊔_ to _⊔ᵘ_
+            ; _⊓_ to _⊓ᵘ_
+            ; ≈-dec to ≈ᵘ-dec
+            ; isLattice to isLatticeᵘ
+            ; ≈-equiv to ≈ᵘ-equiv
+            ; fixedHeight to fixedHeightᵘ
+            )
+    open import Lattice.IterProd _≈₂_ _≈ᵘ_ _⊔₂_ _⊔ᵘ_ _⊓₂_ _⊓ᵘ_ lB isLatticeᵘ
+        as IP
+        using (IterProd)
+    open IsLattice lB using ()
+        renaming
+            ( ≈-trans to ≈₂-trans
+            ; ≈-sym to ≈₂-sym
+            ; FixedHeight to FixedHeight₂
+            )
 
     from : ∀ {ks : List A} → FiniteMap ks → IterProd (length ks)
     from {[]} (([] , _) , _) = tt
-    from {k ∷ ks'} (((k' , v) ∷ fm' , push _ uks') , refl) = (v , from ((fm' , uks'), refl))
+    from {k ∷ ks'} (((k' , v) ∷ fm' , push _ uks') , refl) =
+        (v , from ((fm' , uks'), refl))
 
     to : ∀ {ks : List A} → Unique ks → IterProd (length ks) → FiniteMap ks
     to {[]} _ ⊤ = (([] , empty) , refl)
@@ -65,17 +93,20 @@ module IterProdIsomorphism where
         _⊆ᵐ_ : ∀ {ks₁ ks₂ : List A} → FiniteMap ks₁ → FiniteMap ks₂ → Set
         _⊆ᵐ_ fm₁ fm₂ = subset-impl (proj₁ (proj₁ fm₁)) (proj₁ (proj₁ fm₂))
 
-        _≈ⁱᵖ_ : ∀ {ks : List A} → IterProd (length ks) → IterProd (length ks) → Set
+        _≈ⁱᵖ_ : ∀ {n : ℕ} → IterProd n → IterProd n → Set
-        _≈ⁱᵖ_ {ks} = IP._≈_ (length ks)
+        _≈ⁱᵖ_ {n} = IP._≈_ n
 
-        _⊔ⁱᵖ_ : ∀ {ks : List A} → IterProd (length ks) → IterProd (length ks) → IterProd (length ks)
+        _⊔ⁱᵖ_ : ∀ {ks : List A} →
+                IterProd (length ks) → IterProd (length ks) → IterProd (length ks)
         _⊔ⁱᵖ_ {ks} = IP._⊔_ (length ks)
 
         _∈ᵐ_ : ∀ {ks : List A} → A × B → FiniteMap ks → Set
         _∈ᵐ_ {ks} k,v fm = k,v ∈ proj₁ fm
 
+    -- The left inverse is: from (to x) = x
     from-to-inverseˡ : ∀ {ks : List A} (uks : Unique ks) →
-                      Inverseˡ (_≈ᵐ_ {ks}) (_≈ⁱᵖ_ {ks}) (from {ks}) (to {ks} uks) -- from (to x) = x
+                      Inverseˡ (_≈ᵐ_ {ks}) (_≈ⁱᵖ_ {length ks})
+                               (from {ks}) (to {ks} uks)
     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 =
@@ -87,33 +118,47 @@ module IterProdIsomorphism where
 
     -- The map has its own uniqueness proof, but the call to 'to' needs a standalone
     -- uniqueness proof too. Work with both proofs as needed to thread things through.
+    --
+    -- The right inverse is: to (from x) = x
     from-to-inverseʳ : ∀ {ks : List A} (uks : Unique ks) →
-                       Inverseʳ (_≈ᵐ_ {ks}) (_≈ⁱᵖ_ {ks}) (from {ks}) (to {ks} uks) -- to (from x) = x
+                       Inverseʳ (_≈ᵐ_ {ks}) (_≈ⁱᵖ_ {length ks})
-    from-to-inverseʳ {[]} _ (([] , empty) , kvs≡ks) rewrite kvs≡ks = ((λ k v ()) , (λ k v ()))
+                                (from {ks}) (to {ks} uks)
-    from-to-inverseʳ {k ∷ ks'} uks@(push k≢ks'₁ uks'₁) fm₁@(m₁@((k , v) ∷ fm'₁ , push k≢ks'₂ uks'₂) , refl)
+    from-to-inverseʳ {[]} _ (([] , empty) , kvs≡ks) rewrite kvs≡ks =
-        with to uks'₁ (from ((fm'₁ , uks'₂) , refl)) | from-to-inverseʳ {ks'} uks'₁ ((fm'₁ , uks'₂) , refl)
+        ( (λ k v ())
-    ...   | ((fm'₂ , ufm'₂) , _) | (fm'₂⊆fm'₁ , fm'₁⊆fm'₂) = (m₂⊆m₁ , m₁⊆m₂)
+        , (λ k v ())
+        )
+    from-to-inverseʳ {k ∷ ks'} uks@(push _ uks'₁) fm₁@(((k , v) ∷ fm'₁ , push _ uks'₂) , refl)
+        with to uks'₁ (from ((fm'₁ , uks'₂) , refl))
+          | from-to-inverseʳ {ks'} uks'₁ ((fm'₁ , uks'₂) , refl)
+    ...   | ((fm'₂ , ufm'₂) , _)
+          | (fm'₂⊆fm'₁ , fm'₁⊆fm'₂) = (m₂⊆m₁ , m₁⊆m₂)
                 where
                     kvs₁ = (k , v) ∷ fm'₁
                     kvs₂ = (k , v) ∷ fm'₂
 
                     m₁⊆m₂ : subset-impl kvs₁ kvs₂
-                    m₁⊆m₂ k' v' (here refl) = (v' , (IsLattice.≈-refl lB , here refl))
+                    m₁⊆m₂ k' v' (here refl) =
+                        (v' , (IsLattice.≈-refl lB , here refl))
                     m₁⊆m₂ k' v' (there k',v'∈fm'₁) =
-                        let (v'' , (v'≈v'' , k',v''∈fm'₂)) = fm'₁⊆fm'₂ k' v' k',v'∈fm'₁
+                        let (v'' , (v'≈v'' , k',v''∈fm'₂)) =
+                                fm'₁⊆fm'₂ k' v' k',v'∈fm'₁
                         in (v'' , (v'≈v'' , there k',v''∈fm'₂))
 
                     m₂⊆m₁ : subset-impl kvs₂ kvs₁
-                    m₂⊆m₁ k' v' (here refl) = (v' , (IsLattice.≈-refl lB , here refl))
+                    m₂⊆m₁ k' v' (here refl) =
+                        (v' , (IsLattice.≈-refl lB , here refl))
                     m₂⊆m₁ k' v' (there k',v'∈fm'₂) =
-                        let (v'' , (v'≈v'' , k',v''∈fm'₁)) = fm'₂⊆fm'₁ k' v' k',v'∈fm'₂
+                        let (v'' , (v'≈v'' , k',v''∈fm'₁)) =
+                                fm'₂⊆fm'₁ k' v' k',v'∈fm'₂
                         in (v'' , (v'≈v'' , there k',v''∈fm'₁))
 
     private
-        first-key-in-map : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) → Σ B (λ v → (k , v) ∈ proj₁ fm)
+        first-key-in-map : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) →
+                           Σ B (λ v → (k , v) ∈ proj₁ fm)
         first-key-in-map (((k , v) ∷ _ , _) , refl) = (v , here refl)
 
-        from-first-value : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) → proj₁ (from fm) ≡ proj₁ (first-key-in-map fm)
+        from-first-value : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) →
+                           proj₁ (from fm) ≡ proj₁ (first-key-in-map fm)
         from-first-value {k} {ks} (((k , v) ∷ _ , push _ _) , refl) = refl
 
         -- We need pop because reasoning about two distinct 'refl' pattern
@@ -123,109 +168,183 @@ module IterProdIsomorphism where
         pop : ∀ {k : A} {ks : List A} → FiniteMap (k ∷ ks) → FiniteMap ks
         pop (((_ ∷ fm') , push _ ufm') , refl) = ((fm' , ufm') , refl)
 
-        pop-≈ :  ∀ {k : A} {ks : List A} (fm₁ fm₂ : FiniteMap (k ∷ ks)) → fm₁ ≈ᵐ fm₂ → pop fm₁ ≈ᵐ pop fm₂
+        pop-≈ : ∀ {k : A} {ks : List A} (fm₁ fm₂ : FiniteMap (k ∷ ks)) →
-        pop-≈ {k} {ks} fm₁ fm₂ (fm₁⊆fm₂ , fm₂⊆fm₁) = (narrow fm₁⊆fm₂ , narrow fm₂⊆fm₁)
+                fm₁ ≈ᵐ fm₂ → pop fm₁ ≈ᵐ pop fm₂
+        pop-≈ {k} {ks} fm₁ fm₂ (fm₁⊆fm₂ , fm₂⊆fm₁) =
+            (narrow fm₁⊆fm₂ , narrow fm₂⊆fm₁)
             where
-                narrow₁ : ∀ {fm₁ fm₂ : FiniteMap (k ∷ ks)} → fm₁ ⊆ᵐ fm₂  → pop fm₁ ⊆ᵐ fm₂
+                narrow₁ : ∀ {fm₁ fm₂ : FiniteMap (k ∷ ks)} →
-                narrow₁ {(_ ∷ _ , push _ _) , refl} kvs₁⊆kvs₂ k' v' k',v'∈fm'₁ = kvs₁⊆kvs₂ k' v' (there k',v'∈fm'₁)
+                         fm₁ ⊆ᵐ fm₂ → pop fm₁ ⊆ᵐ fm₂
+                narrow₁ {(_ ∷ _ , push _ _) , refl} kvs₁⊆kvs₂ k' v' k',v'∈fm'₁ =
+                    kvs₁⊆kvs₂ k' v' (there k',v'∈fm'₁)
 
-                narrow₂ : ∀ {fm₁ : FiniteMap ks} {fm₂ : FiniteMap (k ∷ ks)} → fm₁ ⊆ᵐ fm₂  → fm₁ ⊆ᵐ pop fm₂
+                narrow₂ : ∀ {fm₁ : FiniteMap ks} {fm₂ : FiniteMap (k ∷ ks)} →
+                          fm₁ ⊆ᵐ fm₂  → fm₁ ⊆ᵐ pop fm₂
                 narrow₂ {fm₁} {fm₂ = (_ ∷ fm'₂ , push k≢ks _) , kvs≡ks@refl} kvs₁⊆kvs₂ k' v' k',v'∈fm'₁
                     with kvs₁⊆kvs₂ k' v' k',v'∈fm'₁
-                ...   | (v'' , (v'≈v'' , here refl)) rewrite sym (proj₂ fm₁) = ⊥-elim (All¬-¬Any k≢ks (forget {m = proj₁ fm₁} k',v'∈fm'₁))
+                ...   | (v'' , (v'≈v'' , here refl)) rewrite sym (proj₂ fm₁) =
-                ...   | (v'' , (v'≈v'' , there k',v'∈fm'₂)) = (v'' , (v'≈v'' , k',v'∈fm'₂))
+                        ⊥-elim (All¬-¬Any k≢ks (forget {m = proj₁ fm₁} k',v'∈fm'₁))
+                ...   | (v'' , (v'≈v'' , there k',v'∈fm'₂)) =
+                        (v'' , (v'≈v'' , k',v'∈fm'₂))
 
-                narrow : ∀ {fm₁ fm₂ : FiniteMap (k ∷ ks)} → fm₁ ⊆ᵐ fm₂  → pop fm₁ ⊆ᵐ pop fm₂
+                narrow : ∀ {fm₁ fm₂ : FiniteMap (k ∷ ks)} →
+                         fm₁ ⊆ᵐ fm₂ → pop fm₁ ⊆ᵐ pop fm₂
                 narrow {fm₁} {fm₂} x = narrow₂ {pop fm₁} (narrow₁ {fm₂ = fm₂} x)
 
-        k,v∈pop⇒k,v∈ : ∀ {k : A} {ks : List A} {k' : A} {v : B} (fm : FiniteMap (k ∷ ks)) → (k' , v) ∈ᵐ pop fm → (¬ k ≡ k' × ((k' , v) ∈ᵐ fm))
+        k,v∈pop⇒k,v∈ : ∀ {k : A} {ks : List A} {k' : A} {v : B} (fm : FiniteMap (k ∷ ks)) →
+                       (k' , v) ∈ᵐ pop fm → (¬ k ≡ k' × ((k' , v) ∈ᵐ fm))
         k,v∈pop⇒k,v∈ {k} {ks} {k'} {v} (m@((k , _) ∷ fm' , push k≢ks uks') , refl) k',v∈fm =
-            ((λ { refl → All¬-¬Any k≢ks (forget {m = (fm' , uks')} k',v∈fm) }), there k',v∈fm)
+            ( (λ { refl → All¬-¬Any k≢ks (forget {m = (fm' , uks')} k',v∈fm) })
+            , there k',v∈fm
+            )
 
-        k,v∈⇒k,v∈pop : ∀ {k : A} {ks : List A} {k' : A} {v : B} (fm : FiniteMap (k ∷ ks)) → ¬ k ≡ k' → (k' , v) ∈ᵐ fm → (k' , v) ∈ᵐ pop fm
+        k,v∈⇒k,v∈pop : ∀ {k : A} {ks : List A} {k' : A} {v : B} (fm : FiniteMap (k ∷ ks)) →
-        k,v∈⇒k,v∈pop {k} {ks} {k'} {v} (m@((k , _) ∷ fm' , push k≢ks uks') , refl) k≢k' (here refl) = ⊥-elim (k≢k' refl)
+                       ¬ k ≡ k' → (k' , v) ∈ᵐ fm → (k' , v) ∈ᵐ pop fm
-        k,v∈⇒k,v∈pop {k} {ks} {k'} {v} (m@((k , _) ∷ fm' , push k≢ks uks') , refl) k≢k' (there k,v'∈fm') = k,v'∈fm'
+        k,v∈⇒k,v∈pop (m@(_ ∷ _ , push k≢ks _) , refl) k≢k' (here refl) = ⊥-elim (k≢k' refl)
+        k,v∈⇒k,v∈pop (m@(_ ∷ _ , push k≢ks _) , refl) k≢k' (there k,v'∈fm') = k,v'∈fm'
 
-        Provenance-union : ∀ {ks : List A} (fm₁ fm₂ : FiniteMap ks) {k : A} {v : B} → (k , v) ∈ᵐ (fm₁ ⊔ᵐ fm₂) → Σ (B × B) (λ (v₁ , v₂) → ((v ≡ v₁ ⊔₂ v₂) × ((k , v₁) ∈ᵐ fm₁ × (k , v₂) ∈ᵐ fm₂)))
+        FromBothMaps : ∀ (k : A) (v : B) {ks : List A} (fm₁ fm₂ : FiniteMap ks) → Set
+        FromBothMaps k v fm₁ fm₂ =
+            Σ (B × B)
+              (λ (v₁ , v₂) → ( (v ≡ v₁ ⊔₂ v₂) × ((k , v₁) ∈ᵐ fm₁ × (k , v₂) ∈ᵐ fm₂)))
+
+        Provenance-union : ∀ {ks : List A} (fm₁ fm₂ : FiniteMap ks) {k : A} {v : B} →
+                           (k , v) ∈ᵐ (fm₁ ⊔ᵐ fm₂) → FromBothMaps k v fm₁ fm₂
         Provenance-union fm₁@(m₁ , ks₁≡ks) fm₂@(m₂ , ks₂≡ks) {k} {v} k,v∈fm₁fm₂
             with Expr-Provenance k ((` m₁) ∪ (` m₂)) (forget {m = proj₁ (fm₁ ⊔ᵐ fm₂)} k,v∈fm₁fm₂)
-        ...   | (_ , (in₁ (single k,v∈m₁) k∉km₂ , _)) with k∈km₁ ← (forget {m = m₁} k,v∈m₁) rewrite trans ks₁≡ks (sym ks₂≡ks) = ⊥-elim (k∉km₂ k∈km₁)
+        ...   | (_ , (in₁ (single k,v∈m₁) k∉km₂ , _))
-        ...   | (_ , (in₂ k∉km₁ (single k,v∈m₂) , _)) with k∈km₂ ← (forget {m = m₂} k,v∈m₂) rewrite trans ks₁≡ks (sym ks₂≡ks) = ⊥-elim (k∉km₁ k∈km₂)
+                with k∈km₁ ← (forget {m = m₁} k,v∈m₁)
+                rewrite trans ks₁≡ks (sym ks₂≡ks) =
+                ⊥-elim (k∉km₂ k∈km₁)
+        ...   | (_ , (in₂ k∉km₁ (single k,v∈m₂) , _))
+                with k∈km₂ ← (forget {m = m₂} k,v∈m₂)
+                rewrite trans ks₁≡ks (sym ks₂≡ks) =
+                ⊥-elim (k∉km₁ k∈km₂)
         ...   | (v₁⊔v₂ , (bothᵘ {v₁} {v₂} (single k,v₁∈m₁) (single k,v₂∈m₂) , k,v₁⊔v₂∈m₁m₂))
-                rewrite Map-functional {m = proj₁ (fm₁ ⊔ᵐ fm₂)} k,v∈fm₁fm₂ k,v₁⊔v₂∈m₁m₂ = ((v₁ , v₂) , (refl , (k,v₁∈m₁ , k,v₂∈m₂)))
+                rewrite Map-functional {m = proj₁ (fm₁ ⊔ᵐ fm₂)} k,v∈fm₁fm₂ k,v₁⊔v₂∈m₁m₂ =
+                ((v₁ , v₂) , (refl , (k,v₁∈m₁ , k,v₂∈m₂)))
 
-        pop-⊔-distr : ∀ {k : A} {ks : List A} (fm₁ fm₂ : FiniteMap (k ∷ ks)) → pop (fm₁ ⊔ᵐ fm₂) ≈ᵐ (pop fm₁ ⊔ᵐ pop fm₂)
+        pop-⊔-distr : ∀ {k : A} {ks : List A} (fm₁ fm₂ : FiniteMap (k ∷ ks)) →
-        pop-⊔-distr {k} {ks} fm₁@(m₁ , _) fm₂@(m₂ , _) = (pfm₁fm₂⊆pfm₁pfm₂ , pfm₁pfm₂⊆pfm₁fm₂)
+                      pop (fm₁ ⊔ᵐ fm₂) ≈ᵐ (pop fm₁ ⊔ᵐ pop fm₂)
+        pop-⊔-distr {k} {ks} fm₁@(m₁ , _) fm₂@(m₂ , _) =
+            (pfm₁fm₂⊆pfm₁pfm₂ , pfm₁pfm₂⊆pfm₁fm₂)
             where
                 -- pfm₁fm₂⊆pfm₁pfm₂ = {!!}
                 pfm₁fm₂⊆pfm₁pfm₂ : pop (fm₁ ⊔ᵐ fm₂) ⊆ᵐ (pop fm₁ ⊔ᵐ pop fm₂)
                 pfm₁fm₂⊆pfm₁pfm₂ k' v' k',v'∈pfm₁fm₂
                     with (k≢k' , k',v'∈fm₁fm₂) ← k,v∈pop⇒k,v∈ (fm₁ ⊔ᵐ fm₂) k',v'∈pfm₁fm₂
-                    with ((v₁ , v₂) , (refl , (k,v₁∈fm₁ , k,v₂∈fm₂))) ← Provenance-union fm₁ fm₂ k',v'∈fm₁fm₂
+                    with ((v₁ , v₂) , (refl , (k,v₁∈fm₁ , k,v₂∈fm₂)))
+                         ← Provenance-union fm₁ fm₂ k',v'∈fm₁fm₂
                     with k',v₁∈pfm₁ ← k,v∈⇒k,v∈pop fm₁ k≢k' k,v₁∈fm₁
                     with k',v₂∈pfm₂ ← k,v∈⇒k,v∈pop fm₂ k≢k' k,v₂∈fm₂
-                    = (v₁ ⊔₂ v₂ , (IsLattice.≈-refl lB , ⊔-combines {m₁ = proj₁ (pop fm₁)} {m₂ = proj₁ (pop fm₂)} k',v₁∈pfm₁ k',v₂∈pfm₂))
+                    =
+                        ( v₁ ⊔₂ v₂
+                        , (IsLattice.≈-refl lB
+                          , ⊔-combines {m₁ = proj₁ (pop fm₁)}
+                                       {m₂ = proj₁ (pop fm₂)}
+                                       k',v₁∈pfm₁ k',v₂∈pfm₂
+                          )
+                        )
 
                 pfm₁pfm₂⊆pfm₁fm₂ : (pop fm₁ ⊔ᵐ pop fm₂) ⊆ᵐ pop (fm₁ ⊔ᵐ fm₂)
                 pfm₁pfm₂⊆pfm₁fm₂ k' v' k',v'∈pfm₁pfm₂
-                    with ((v₁ , v₂) , (refl , (k,v₁∈pfm₁ , k,v₂∈pfm₂))) ← Provenance-union (pop fm₁) (pop fm₂) k',v'∈pfm₁pfm₂
+                    with ((v₁ , v₂) , (refl , (k,v₁∈pfm₁ , k,v₂∈pfm₂)))
+                         ← Provenance-union (pop fm₁) (pop fm₂) k',v'∈pfm₁pfm₂
                     with (k≢k' , k',v₁∈fm₁) ← k,v∈pop⇒k,v∈ fm₁ k,v₁∈pfm₁
                     with (_    , k',v₂∈fm₂) ← k,v∈pop⇒k,v∈ fm₂ k,v₂∈pfm₂
-                    = (v₁ ⊔₂ v₂ , (IsLattice.≈-refl lB , k,v∈⇒k,v∈pop (fm₁ ⊔ᵐ fm₂) k≢k' (⊔-combines {m₁ = m₁} {m₂ = m₂} k',v₁∈fm₁ k',v₂∈fm₂)))
+                    =
+                        ( v₁ ⊔₂ v₂
+                        , ( IsLattice.≈-refl lB
+                          , k,v∈⇒k,v∈pop (fm₁ ⊔ᵐ fm₂) k≢k'
+                                         (⊔-combines {m₁ = m₁} {m₂ = m₂}
+                                                     k',v₁∈fm₁ k',v₂∈fm₂)
+                          )
+                        )
 
-        from-rest : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) → proj₂ (from fm) ≡ from (pop fm)
+        from-rest : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) →
+                    proj₂ (from fm) ≡ from (pop fm)
         from-rest (((_ ∷ fm') , push _ ufm') , refl) = refl
 
-    from-preserves-≈ : ∀ {ks : List A} → {fm₁ fm₂ : FiniteMap ks} → fm₁ ≈ᵐ fm₂ → (_≈ⁱᵖ_ {ks}) (from fm₁) (from fm₂)
+    from-preserves-≈ : ∀ {ks : List A} → {fm₁ fm₂ : FiniteMap ks} →
-    from-preserves-≈ {[]} {([] , _) , _} {([] , _) , _} _ = IsEquivalence.≈-refl ≈ᵘ-equiv
+                       fm₁ ≈ᵐ fm₂ → (_≈ⁱᵖ_ {length ks}) (from fm₁) (from fm₂)
+    from-preserves-≈ {[]} {_} {_} _ = IsEquivalence.≈-refl ≈ᵘ-equiv
     from-preserves-≈ {k ∷ ks'} {fm₁@(m₁ , _)} {fm₂@(m₂ , _)} fm₁≈fm₂@(kvs₁⊆kvs₂ , kvs₂⊆kvs₁)
-        with first-key-in-map fm₁ | first-key-in-map fm₂ | from-first-value fm₁ | from-first-value fm₂
+        with first-key-in-map fm₁
+          | first-key-in-map fm₂
+          | from-first-value fm₁
+          | from-first-value fm₂
     ...   | (v₁ , k,v₁∈fm₁) | (v₂ , k,v₂∈fm₂) | refl | refl
             with kvs₁⊆kvs₂ _ _ k,v₁∈fm₁
     ...       | (v₁' , (v₁≈v₁' , k,v₁'∈fm₂))
                 rewrite Map-functional {m = m₂} k,v₂∈fm₂ k,v₁'∈fm₂
                 rewrite from-rest fm₁ rewrite from-rest fm₂
-                = (v₁≈v₁' , from-preserves-≈ {ks'} {pop fm₁} {pop fm₂} (pop-≈ fm₁ fm₂ fm₁≈fm₂))
+                =
+                    ( v₁≈v₁'
+                    , from-preserves-≈ {ks'} {pop fm₁} {pop fm₂}
+                                       (pop-≈ fm₁ fm₂ fm₁≈fm₂)
+                    )
 
-    to-preserves-≈ : ∀ {ks : List A} (uks : Unique ks) {ip₁ ip₂ : IterProd (length ks)} → _≈ⁱᵖ_ {ks} ip₁ ip₂ → to uks ip₁ ≈ᵐ to uks ip₂
+    to-preserves-≈ : ∀ {ks : List A} (uks : Unique ks) {ip₁ ip₂ : IterProd (length ks)} →
+                     _≈ⁱᵖ_ {length ks} ip₁ ip₂ → to uks ip₁ ≈ᵐ to uks ip₂
     to-preserves-≈ {[]} empty {tt} {tt} _ = ((λ k v ()), (λ k v ()))
     to-preserves-≈ {k ∷ ks'} uks@(push k≢ks' uks') {ip₁@(v₁ , rest₁)} {ip₂@(v₂ , rest₂)} (v₁≈v₂ , rest₁≈rest₂) = (fm₁⊆fm₂ , fm₂⊆fm₁)
         where
-            fm₁⊆fm₂ : to uks ip₁ ⊆ᵐ to uks ip₂
+            inductive-step : ∀ {v₁ v₂ : B} {rest₁ rest₂ : IterProd (length ks')} →
-            fm₁⊆fm₂ k v k,v∈kvs₁
+                               v₁ ≈₂ v₂ → _≈ⁱᵖ_ {length ks'} rest₁ rest₂ →
+                               to uks (v₁ , rest₁) ⊆ᵐ to uks (v₂ , rest₂)
+            inductive-step {v₁} {v₂} {rest₁} {rest₂} v₁≈v₂ rest₁≈rest₂ k v k,v∈kvs₁
                 with ((fm'₁ , ufm'₁) , fm'₁≡ks') ← to uks' rest₁ in p₁
                 with ((fm'₂ , ufm'₂) , fm'₂≡ks') ← to uks' rest₂ in p₂
                 with k,v∈kvs₁
             ...   | here refl = (v₂ , (v₁≈v₂ , here refl))
-            ...   | there k,v∈fm'₁ with refl ← p₁ with refl ← p₂ = let (v' , (v≈v' , k,v'∈kvs₁)) = proj₁ (to-preserves-≈ uks' {rest₁} {rest₂} rest₁≈rest₂) k v k,v∈fm'₁ in (v' , (v≈v' , there k,v'∈kvs₁))
+            ...   | there k,v∈fm'₁ with refl ← p₁ with refl ← p₂ =
+                    let
+                        (fm'₁⊆fm'₂ , _) = to-preserves-≈ uks' {rest₁} {rest₂}
+                                                         rest₁≈rest₂
+                        (v' , (v≈v' , k,v'∈kvs₁)) = fm'₁⊆fm'₂ k v k,v∈fm'₁
+                    in
+                        (v' , (v≈v' , there k,v'∈kvs₁))
+
+            fm₁⊆fm₂ : to uks ip₁ ⊆ᵐ to uks ip₂
+            fm₁⊆fm₂ = inductive-step v₁≈v₂ rest₁≈rest₂
 
             fm₂⊆fm₁ : to uks ip₂ ⊆ᵐ to uks ip₁
-            fm₂⊆fm₁ k v k,v∈kvs₂
+            fm₂⊆fm₁ = inductive-step (≈₂-sym v₁≈v₂)
-                with ((fm'₁ , ufm'₁) , fm'₁≡ks') ← to uks' rest₁ in p₁
+                                     (IP.≈-sym (length ks') rest₁≈rest₂)
-                with ((fm'₂ , ufm'₂) , fm'₂≡ks') ← to uks' rest₂ in p₂
-                with k,v∈kvs₂
-            ...   | here refl = (v₁ , (IsLattice.≈-sym lB v₁≈v₂ , here refl))
-            ...   | there k,v∈fm'₂ with refl ← p₁ with refl ← p₂ = let (v' , (v≈v' , k,v'∈kvs₂)) = proj₂ (to-preserves-≈ uks' {rest₁} {rest₂} rest₁≈rest₂) k v k,v∈fm'₂ in (v' , (v≈v' , there k,v'∈kvs₂))
 
-    from-⊔-distr : ∀ {ks : List A} → (fm₁ fm₂ : FiniteMap ks) → _≈ⁱᵖ_ {ks} (from (fm₁ ⊔ᵐ fm₂)) (_⊔ⁱᵖ_ {ks} (from fm₁) (from fm₂))
+    from-⊔-distr : ∀ {ks : List A} → (fm₁ fm₂ : FiniteMap ks) →
+                  _≈ⁱᵖ_ {length ks} (from (fm₁ ⊔ᵐ fm₂))
+                                    (_⊔ⁱᵖ_ {ks} (from fm₁) (from fm₂))
     from-⊔-distr {[]} fm₁ fm₂ = IsEquivalence.≈-refl ≈ᵘ-equiv
     from-⊔-distr {k ∷ ks} fm₁@(m₁ , _) fm₂@(m₂ , _)
-        with first-key-in-map (fm₁ ⊔ᵐ fm₂) | first-key-in-map fm₁ | first-key-in-map fm₂ | from-first-value (fm₁ ⊔ᵐ fm₂) | from-first-value fm₁ | from-first-value fm₂
+        with first-key-in-map (fm₁ ⊔ᵐ fm₂)
+          | first-key-in-map fm₁
+          | first-key-in-map fm₂
+          | from-first-value (fm₁ ⊔ᵐ fm₂)
+          | from-first-value fm₁ | from-first-value fm₂
     ...   | (v , k,v∈fm₁fm₂) | (v₁ , k,v₁∈fm₁) | (v₂ , k,v₂∈fm₂) | refl | refl | refl
             with Expr-Provenance k ((` m₁) ∪ (` m₂)) (forget {m = proj₁ (fm₁ ⊔ᵐ fm₂)} k,v∈fm₁fm₂)
-    ...       | (_ , (in₁ _ k∉km₂ , _)) = ⊥-elim (k∉km₂ (forget {m = m₂} k,v₂∈fm₂))
+    ...       | (_ , (in₁ _ k∉km₂ , _)) = ⊥-elim (k∉km₂ (forget {m = m₂}
-    ...       | (_ , (in₂ k∉km₁ _ , _)) = ⊥-elim (k∉km₁ (forget {m = m₁} k,v₁∈fm₁))
+                                                                k,v₂∈fm₂))
+    ...       | (_ , (in₂ k∉km₁ _ , _)) = ⊥-elim (k∉km₁ (forget {m = m₁}
+                                                                k,v₁∈fm₁))
     ...       | (v₁⊔v₂ , (bothᵘ {v₁'} {v₂'} (single k,v₁'∈m₁) (single k,v₂'∈m₂) , k,v₁⊔v₂∈m₁m₂))
                 rewrite Map-functional {m = m₁} k,v₁∈fm₁ k,v₁'∈m₁
                 rewrite Map-functional {m = m₂} k,v₂∈fm₂ k,v₂'∈m₂
                 rewrite Map-functional {m = proj₁ (fm₁ ⊔ᵐ fm₂)} k,v∈fm₁fm₂ k,v₁⊔v₂∈m₁m₂
                 rewrite from-rest (fm₁ ⊔ᵐ fm₂) rewrite from-rest fm₁ rewrite from-rest fm₂
                 = ( IsLattice.≈-refl lB
-                  , IsEquivalence.≈-trans (IP.≈-equiv (length ks)) (from-preserves-≈ {_} {pop (fm₁ ⊔ᵐ fm₂)} {pop fm₁ ⊔ᵐ pop fm₂} (pop-⊔-distr fm₁ fm₂)) ((from-⊔-distr (pop fm₁) (pop fm₂)))
+                  , IsEquivalence.≈-trans
+                        (IP.≈-equiv (length ks))
+                        (from-preserves-≈ {_} {pop (fm₁ ⊔ᵐ fm₂)}
+                                              {pop fm₁ ⊔ᵐ pop fm₂}
+                                              (pop-⊔-distr fm₁ fm₂))
+                        ((from-⊔-distr (pop fm₁) (pop fm₂)))
                   )
 
 
-    to-⊔-distr : ∀ {ks : List A} (uks : Unique ks) → (ip₁ ip₂ : IterProd (length ks)) → to uks (_⊔ⁱᵖ_ {ks} ip₁ ip₂) ≈ᵐ (to uks ip₁ ⊔ᵐ to uks ip₂)
+    to-⊔-distr : ∀ {ks : List A} (uks : Unique ks) → (ip₁ ip₂ : IterProd (length ks)) →
+                 to uks (_⊔ⁱᵖ_ {ks} ip₁ ip₂) ≈ᵐ (to uks ip₁ ⊔ᵐ to uks ip₂)
     to-⊔-distr {[]} empty tt tt = ((λ k v ()), (λ k v ()))
     to-⊔-distr {ks@(k ∷ ks')} uks@(push k≢ks' uks') ip₁@(v₁ , rest₁) ip₂@(v₂ , rest₂) = (fm⊆fm₁fm₂ , fm₁fm₂⊆fm)
         where
@@ -239,27 +358,45 @@ module IterProdIsomorphism where
             fm⊆fm₁fm₂ k v (here refl) =
                 (v₁ ⊔₂ v₂
                 , (IsLattice.≈-refl lB
-                  , ⊔-combines {k} {v₁} {v₂} {proj₁ fm₁} {proj₁ fm₂} (here refl) (here refl)
+                  , ⊔-combines {k} {v₁} {v₂} {proj₁ fm₁} {proj₁ fm₂}
+                               (here refl) (here refl)
                   )
                 )
             fm⊆fm₁fm₂ k' v (there k',v∈fm')
                 with (fm'⊆fm'₁fm'₂ , _) ← to-⊔-distr uks' rest₁ rest₂
-                with (v' , (v₁⊔v₂≈v' , k',v'∈fm'₁fm'₂)) ← fm'⊆fm'₁fm'₂ k' v k',v∈fm'
+                with (v' , (v₁⊔v₂≈v' , k',v'∈fm'₁fm'₂))
-                with (_ , (refl , (v₁∈fm'₁ , v₂∈fm'₂))) ← Provenance-union fm₁' fm₂' k',v'∈fm'₁fm'₂ =
+                     ← fm'⊆fm'₁fm'₂ k' v k',v∈fm'
-                (v' , (v₁⊔v₂≈v' , ⊔-combines {m₁ = proj₁ fm₁} {m₂ = proj₁ fm₂} (there v₁∈fm'₁) (there v₂∈fm'₂)))
+                with (_ , (refl , (v₁∈fm'₁ , v₂∈fm'₂)))
+                     ← Provenance-union fm₁' fm₂' k',v'∈fm'₁fm'₂ =
+                ( v'
+                , ( v₁⊔v₂≈v'
+                  , ⊔-combines {m₁ = proj₁ fm₁} {m₂ = proj₁ fm₂}
+                               (there v₁∈fm'₁) (there v₂∈fm'₂)
+                  )
+                )
 
             fm₁fm₂⊆fm : (fm₁ ⊔ᵐ fm₂) ⊆ᵐ fm
             fm₁fm₂⊆fm k' v k',v∈fm₁fm₂
-                with (_ , fm'₁fm'₂⊆fm') ← to-⊔-distr uks' rest₁ rest₂
+                with (_ , fm'₁fm'₂⊆fm')
-                with (_ , (refl , (v₁∈fm₁ , v₂∈fm₂))) ← Provenance-union fm₁ fm₂ k',v∈fm₁fm₂
+                     ← to-⊔-distr uks' rest₁ rest₂
+                with (_ , (refl , (v₁∈fm₁ , v₂∈fm₂)))
+                     ← Provenance-union fm₁ fm₂ k',v∈fm₁fm₂
                 with v₁∈fm₁ | v₂∈fm₂
-            ...   | here refl | here refl = (v , (IsLattice.≈-refl lB , here refl))
+            ...   | here refl | here refl =
-            ...   | here refl | there k',v₂∈fm₂' = ⊥-elim (All¬-¬Any k≢ks' (subst (λ list → k' ∈ˡ list) (proj₂ fm₂') (forget {m = proj₁ fm₂'} k',v₂∈fm₂')))
+                    (v , (IsLattice.≈-refl lB , here refl))
-            ...   | there k',v₁∈fm₁' | here refl = ⊥-elim (All¬-¬Any k≢ks' (subst (λ list → k' ∈ˡ list) (proj₂ fm₁') (forget {m = proj₁ fm₁'} k',v₁∈fm₁')))
+            ...   | here refl | there k',v₂∈fm₂' =
+                    ⊥-elim (All¬-¬Any k≢ks' (subst (k' ∈ˡ_) (proj₂ fm₂')
+                                                   (forget {m = proj₁ fm₂'} k',v₂∈fm₂')))
+            ...   | there k',v₁∈fm₁' | here refl =
+                    ⊥-elim (All¬-¬Any k≢ks' (subst (k' ∈ˡ_) (proj₂ fm₁')
+                                                   (forget {m = proj₁ fm₁'} k',v₁∈fm₁')))
             ...   | there k',v₁∈fm₁' | there k',v₂∈fm₂' =
                         let
-                            k',v₁v₂∈fm₁'fm₂' = ⊔-combines {m₁ = proj₁ fm₁'} {m₂ = proj₁ fm₂'} k',v₁∈fm₁' k',v₂∈fm₂'
+                            k',v₁v₂∈fm₁'fm₂' =
-                            (v' , (v₁⊔v₂≈v' , v'∈fm')) = fm'₁fm'₂⊆fm' _ _ k',v₁v₂∈fm₁'fm₂'
+                                ⊔-combines {m₁ = proj₁ fm₁'} {m₂ = proj₁ fm₂'}
+                                           k',v₁∈fm₁' k',v₂∈fm₂'
+                            (v' , (v₁⊔v₂≈v' , v'∈fm')) =
+                                fm'₁fm'₂⊆fm' _ _ k',v₁v₂∈fm₁'fm₂'
                         in
                             (v' , (v₁⊔v₂≈v' , there v'∈fm'))
 

Main.agda

@@ -56,14 +56,4 @@ dumbFunction-Monotonic {m₁} {m₂} m₁≼m₂ = ⊔-Monotonicˡ dumb {m₁} {
 
 open import Fixedpoint {0ℓ} {FiniteHeightMap xyzw} {8} {_≈_} {_⊔_} {_⊓_} (≈-dec fhlᵘ xyzw-Unique ≈ᵘ-dec) (FiniteHeightLattice.isFiniteHeightLattice fhlⁱᵖ) dumbFunction (λ {m₁} {m₂} m₁≼m₂ → dumbFunction-Monotonic {m₁} {m₂} m₁≼m₂)
 
--- module Fixedpoint {a} {A : Set a}
---                   {h : ℕ}
---                   {_≈_ : A → A → Set a}
---                   {_⊔_ : A → A → A} {_⊓_ : A → A → A}
---                   (≈-dec : IsDecidable _≈_)
---                   (flA : IsFiniteHeightLattice A h _≈_ _⊔_ _⊓_)
---                   (f : A → A)
---                   (Monotonicᶠ : Monotonic (IsFiniteHeightLattice._≼_ flA)
---                                           (IsFiniteHeightLattice._≼_ flA) f) where
-
 main = run {0ℓ} (putStrLn (showMap aᶠ))