Require bottom element to actually be bottom; finish proof

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

Equivalence.agda

@@ -2,7 +2,7 @@ module Equivalence where
 
 open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
 open import Relation.Binary.Definitions
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans)
 
 module _ {a} (A : Set a) (_≈_ : A → A → Set a) where
     IsReflexive : Set a
@@ -19,3 +19,10 @@ module _ {a} (A : Set a) (_≈_ : A → A → Set a) where
             ≈-refl : IsReflexive
             ≈-sym : IsSymmetric
             ≈-trans : IsTransitive
+
+isEquivalence-≡ : ∀ {a} {A : Set a} → IsEquivalence A _≡_
+isEquivalence-≡ = record
+    { ≈-refl = refl
+    ; ≈-sym = sym
+    ; ≈-trans = trans
+    }

Language/Graphs.agda

@@ -18,7 +18,7 @@ open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; refl;
 open import Relation.Nullary using (¬_)
 
 open import Lattice
-open import Utils using (Unique; push; Unique-map; x∈xs⇒fx∈fxs; ∈-cartesianProduct)
+open import Utils using (Unique; push; Unique-map; x∈xs⇒fx∈fxs; ∈-cartesianProduct; fins; fins-complete)
 
 record Graph : Set where
     constructor MkGraph

Lattice.agda

@@ -96,6 +96,12 @@ record IsSemilattice {a} (A : Set a)
                     (a₁ ⊔ a) ⊔ (a₂ ⊔ a)
                 ∎
 
+    -- need to show: a₁ ⊔ (a₁ ⊔ a₂) ≈ a₁ ⊔ a₂
+    -- (a₁ ⊔ a₁) ⊔ a₂ ≈ a₁ ⊔ (a₁ ⊔ a₂)
+
+    x≼x⊔y : ∀ (a₁ a₂ : A) → a₁ ≼ (a₁ ⊔ a₂)
+    x≼x⊔y a₁ a₂ = ≈-sym (≈-trans (≈-⊔-cong (≈-sym (⊔-idemp a₁)) (≈-refl {a₂})) (⊔-assoc a₁ a₁ a₂))
+
     ≼-refl : ∀ (a : A) → a ≼ a
     ≼-refl a = ⊔-idemp a
 
@@ -113,6 +119,18 @@ record IsSemilattice {a} (A : Set a)
             a₃
         ∎
 
+    ≼-antisym : ∀ {a₁ a₂ : A} → a₁ ≼ a₂ → a₂ ≼ a₁ → a₁ ≈ a₂
+    ≼-antisym {a₁} {a₂} a₁⊔a₂≈a₂ a₂⊔a₁≈a₁ =
+        begin
+            a₁
+        ∼⟨ ≈-sym a₂⊔a₁≈a₁ ⟩
+            a₂ ⊔ a₁
+        ∼⟨ ⊔-comm _ _ ⟩
+            a₁ ⊔ a₂
+        ∼⟨ a₁⊔a₂≈a₂ ⟩
+            a₂
+        ∎
+
     ≼-cong : ∀ {a₁ a₂ a₃ a₄ : A} → a₁ ≈ a₂ → a₃ ≈ a₄ → a₁ ≼ a₃ → a₂ ≼ a₄
     ≼-cong {a₁} {a₂} {a₃} {a₄} a₁≈a₂ a₃≈a₄ a₁⊔a₃≈a₃ =
         begin
@@ -237,16 +255,25 @@ record IsFiniteHeightLattice {a} (A : Set a)
     field
         {{fixedHeight}} : FixedHeight h
 
+    private
+        module MyChain = Chain _≈_ ≈-equiv _≺_ ≺-cong
+
+    open MyChain.Height fixedHeight using (⊥; ⊤) public
+
+    Known-⊥ : Set a
+    Known-⊥ = ∀ (a : A) → ⊥ ≼ a
+
+    Known-⊤ : Set a
+    Known-⊤ = ∀ (a : A) → a ≼ ⊤
+
     -- If the equality is decidable, we can prove that the top and bottom
     -- elements of the chain are least and greatest elements of the lattice
     module _ {{≈-Decidable : IsDecidable _≈_}} where
         open IsDecidable ≈-Decidable using () renaming (R-dec to ≈-dec)
 
-        module MyChain = Chain _≈_ ≈-equiv _≺_ ≺-cong
-        open MyChain.Height fixedHeight using (⊥; ⊤) public
         open MyChain.Height fixedHeight using (bounded; longestChain)
 
-        ⊥≼ : ∀ (a : A) → ⊥ ≼ a
+        ⊥≼ : Known-⊥
         ⊥≼ a with ≈-dec a ⊥
         ...   | yes a≈⊥ = ≼-cong a≈⊥ ≈-refl (≼-refl a)
         ...   | no a̷≈⊥ with ≈-dec ⊥ (a ⊓ ⊥)

Lattice/Builder.agda

@@ -456,7 +456,7 @@ record Graph : Set where
     Total-⊓? : Dec Total-⊓
     Total-⊓? = P-Total? Have-⊓?
 
-    module AssumeWellFormed (noCycles : NoCycles) (total-⊔ : Total-⊔) (total-⊓ : Total-⊓) where
+    module Basic (noCycles : NoCycles) (total-⊔ : Total-⊔) (total-⊓ : Total-⊓) where
         n₁→n₂×n₂→n₁⇒n₁≡n₂ : ∀ {n₁ n₂} → PathExists n₁ n₂ → PathExists n₂ n₁ → n₁ ≡ n₂
         n₁→n₂×n₂→n₁⇒n₁≡n₂ n₁→n₂ n₂→n₁
             with n₁→n₂ | n₂→n₁ | noCycles (n₁→n₂ ++ n₂→n₁)
@@ -520,13 +520,13 @@ record Graph : Set where
         ⊥-is-⊥ : Is-⊥ ⊥
         ⊥-is-⊥ = foldr₁⊓-Suc nodes-nonempty
 
-        ⊔-refl : ∀ n → n ⊔ n ≡ n
-        ⊔-refl n
+        ⊔-idemp : ∀ n → n ⊔ n ≡ n
+        ⊔-idemp n
             with (n' , ((n'→n , _) , n''→n×n''→n⇒n''→n')) ← total-⊔ n n
             = n₁→n₂×n₂→n₁⇒n₁≡n₂ n'→n (n''→n×n''→n⇒n''→n' n (done , done))
 
-        ⊓-refl : ∀ n → n ⊓ n ≡ n
-        ⊓-refl n
+        ⊓-idemp : ∀ n → n ⊓ n ≡ n
+        ⊓-idemp n
             with (n' , ((n→n' , _) , n→n''×n→n''⇒n'→n'')) ← total-⊓ n n
             = n₁→n₂×n₂→n₁⇒n₁≡n₂ (n→n''×n→n''⇒n'→n'' n (done , done)) n→n'
 
@@ -543,3 +543,343 @@ record Graph : Set where
             with (n₂₁ , ((n₂→n₂n₁ , n₁→n₂n₁) , n₂→n'×n₁→n'⇒n₂₁→n')) ← total-⊓ n₂ n₁
             = n₁→n₂×n₂→n₁⇒n₁≡n₂ (n₁→n'×n₂→n'⇒n₁₂→n' n₂₁ (n₁→n₂n₁ , n₂→n₂n₁))
                                 (n₂→n'×n₁→n'⇒n₂₁→n' n₁₂ (n₂→n₁n₂ , n₁→n₁n₂))
+
+        ⊔-assoc : ∀ n₁ n₂ n₃ → (n₁ ⊔ n₂) ⊔ n₃ ≡ n₁ ⊔ (n₂ ⊔ n₃)
+        ⊔-assoc n₁ n₂ n₃
+            with (n₁₂ , ((n₁₂→n₁ , n₁₂→n₂) , n'→n₁×n'→n₂⇒n'→n₁₂)) ← total-⊔ n₁ n₂
+            with (n₁₂,₃ , ((n₁₂,₃→n₁₂ , n₁₂,₃→n₃) , n'→n₁₂×n'→n₃⇒n'→n₁₂,₃)) ← total-⊔ n₁₂ n₃
+            with (n₂₃ , ((n₂₃→n₂ , n₂₃→n₃) , n'→n₂×n'→n₃⇒n'→n₂₃)) ← total-⊔ n₂ n₃
+            with (n₁,₂₃ , ((n₁,₂₃→n₁ , n₁,₂₃→n₂₃) , n'→n₁×n'→n₂₃⇒n'→n₁,₂₃)) ← total-⊔ n₁ n₂₃
+            =
+                let n₁₂,₃→n₂₃ = n'→n₂×n'→n₃⇒n'→n₂₃ n₁₂,₃ (n₁₂,₃→n₁₂ ++ n₁₂→n₂ , n₁₂,₃→n₃)
+                    n₁₂,₃→n₁,₂₃ = n'→n₁×n'→n₂₃⇒n'→n₁,₂₃ n₁₂,₃ (n₁₂,₃→n₁₂ ++ n₁₂→n₁ , n₁₂,₃→n₂₃)
+                    n₁,₂₃→n₁₂ = n'→n₁×n'→n₂⇒n'→n₁₂ n₁,₂₃ (n₁,₂₃→n₁ , n₁,₂₃→n₂₃ ++ n₂₃→n₂)
+                    n₁,₂₃→n₁₂,₃ = n'→n₁₂×n'→n₃⇒n'→n₁₂,₃ n₁,₂₃ (n₁,₂₃→n₁₂ , n₁,₂₃→n₂₃ ++ n₂₃→n₃)
+                in n₁→n₂×n₂→n₁⇒n₁≡n₂ n₁₂,₃→n₁,₂₃ n₁,₂₃→n₁₂,₃
+
+        ⊓-assoc : ∀ n₁ n₂ n₃ → (n₁ ⊓ n₂) ⊓ n₃ ≡ n₁ ⊓ (n₂ ⊓ n₃)
+        ⊓-assoc n₁ n₂ n₃
+          with (n₁₂ , ((n₁→n₁₂ , n₂→n₁₂) , n₁→n'×n₂→n'⇒n₁₂→n')) ← total-⊓ n₁ n₂
+          with (n₁₂,₃ , ((n₁₂→n₁₂,₃ , n₃→n₁₂,₃) , n₁₂→n'×n₃→n'⇒n₁₂,₃→n')) ← total-⊓ n₁₂ n₃
+          with (n₂₃ , ((n₂→n₂₃ , n₃→n₂₃) ,  n₂→n'×n₃→n'⇒n₂₃→n')) ← total-⊓ n₂ n₃
+          with (n₁,₂₃ , ((n₁→n₁,₂₃ , n₂₃→n₁,₂₃) ,  n₁→n'×n₂₃→n'⇒n₁,₂₃→n')) ← total-⊓ n₁ n₂₃
+          =
+            let n₁₂→n₁,₂₃ = n₁→n'×n₂→n'⇒n₁₂→n' n₁,₂₃ (n₁→n₁,₂₃ , n₂→n₂₃ ++ n₂₃→n₁,₂₃)
+                n₁₂,₃→n₁,₂₃ = n₁₂→n'×n₃→n'⇒n₁₂,₃→n' n₁,₂₃ (n₁₂→n₁,₂₃ , n₃→n₂₃ ++ n₂₃→n₁,₂₃)
+                n₂₃→n₁₂,₃ = n₂→n'×n₃→n'⇒n₂₃→n' n₁₂,₃ (n₂→n₁₂ ++ n₁₂→n₁₂,₃ , n₃→n₁₂,₃)
+                n₁,₂₃→n₁₂,₃ = n₁→n'×n₂₃→n'⇒n₁,₂₃→n' n₁₂,₃ (n₁→n₁₂ ++ n₁₂→n₁₂,₃ , n₂₃→n₁₂,₃)
+            in n₁→n₂×n₂→n₁⇒n₁≡n₂ n₁₂,₃→n₁,₂₃ n₁,₂₃→n₁₂,₃
+
+        absorb-⊔-⊓ : ∀ n₁ n₂ → n₁ ⊔ (n₁ ⊓ n₂) ≡ n₁
+        absorb-⊔-⊓ n₁ n₂
+            with (n₁₂ , ((n₁→n₁₂ , n₂→n₁₂) , n₁→n'×n₂→n'⇒n₁₂→n')) ← total-⊓ n₁ n₂
+            with (n₁,₁₂ , ((n₁,₁₂→n₁ , n₁,₁₂→n₁₂) , n'→n₁×n'→n₁₂⇒n'→n₁,₁₂)) ← total-⊔ n₁ n₁₂
+            = n₁→n₂×n₂→n₁⇒n₁≡n₂ n₁,₁₂→n₁ (n'→n₁×n'→n₁₂⇒n'→n₁,₁₂ n₁ (done , n₁→n₁₂))
+
+        absorb-⊓-⊔ : ∀ n₁ n₂ → n₁ ⊓ (n₁ ⊔ n₂) ≡ n₁
+        absorb-⊓-⊔ n₁ n₂
+            with (n₁₂ , ((n₁₂→n₁ , n₁₂→n₂) , n'→n₁×n'→n₂⇒n'→n₁₂)) ← total-⊔ n₁ n₂
+            with (n₁,₁₂ , ((n₁→n₁,₁₂ , n₁₂→n₁,₁₂) , n₁→n'×n₁₂→n'⇒n₁,₁₂→n')) ← total-⊓ n₁ n₁₂
+            = n₁→n₂×n₂→n₁⇒n₁≡n₂ (n₁→n'×n₁₂→n'⇒n₁,₁₂→n' n₁ (done , n₁₂→n₁)) n₁→n₁,₁₂
+
+        instance
+            isJoinSemilattice : IsSemilattice Node _≡_ _⊔_
+            isJoinSemilattice = record
+                { ≈-equiv = isEquivalence-≡
+                ; ≈-⊔-cong = (λ { refl refl → refl })
+                ; ⊔-idemp = ⊔-idemp
+                ; ⊔-comm = ⊔-comm
+                ; ⊔-assoc = ⊔-assoc
+                }
+
+            isMeetSemilattice : IsSemilattice Node _≡_ _⊓_
+            isMeetSemilattice = record
+                { ≈-equiv = isEquivalence-≡
+                ; ≈-⊔-cong = (λ { refl refl → refl })
+                ; ⊔-idemp = ⊓-idemp
+                ; ⊔-comm = ⊓-comm
+                ; ⊔-assoc = ⊓-assoc
+                }
+
+            isLattice : IsLattice Node _≡_ _⊔_ _⊓_
+            isLattice = record
+                { absorb-⊔-⊓ = absorb-⊔-⊓
+                ; absorb-⊓-⊔ = absorb-⊓-⊔
+                }
+
+    module Tagged (noCycles : NoCycles) (total-⊔ : Total-⊔) (total-⊓ : Total-⊓) (𝓛 : Node → Σ Set λ L → Σ (FiniteHeightLattice L) λ fhl → FiniteHeightLattice.Known-⊥ fhl × FiniteHeightLattice.Known-⊤ fhl) where
+        open Basic noCycles total-⊔ total-⊓ using () renaming (_⊔_ to _⊔ᵇ_; _⊓_ to _⊓ᵇ_; ⊔-idemp to ⊔ᵇ-idemp; ⊔-comm to ⊔ᵇ-comm; ⊔-assoc to ⊔ᵇ-assoc; _≼_ to _≼ᵇ_; isJoinSemilattice to isJoinSemilatticeᵇ; isMeetSemilattice to isMeetSemilatticeᵇ; isLattice to isLatticeᵇ)
+
+        open IsLattice isLatticeᵇ using () renaming (≈-⊔-cong to ≡-⊔ᵇ-cong; x≼x⊔y to x≼ᵇx⊔ᵇy; ≼-antisym to ≼ᵇ-antisym; ⊔-Monotonicʳ to ⊔ᵇ-Monotonicʳ)
+
+        Elem : Set
+        Elem = Σ Node λ n → (proj₁ (𝓛 n))
+
+        LatticeT : Node → Set
+        LatticeT n = proj₁ (𝓛 n)
+
+        FHL : (n : Node) → FiniteHeightLattice (LatticeT n)
+        FHL n = proj₁ (proj₂ (𝓛 n))
+
+        ⊥≼x : ∀ {n : Node} (l : LatticeT n) → FiniteHeightLattice._≼_ (FHL n) (FiniteHeightLattice.⊥ (FHL n)) l
+        ⊥≼x {n} = proj₁ (proj₂ (proj₂ (𝓛 n)))
+
+        data _≈_ : Elem → Elem → Set where
+            ≈-lift : ∀ {n : Node} {l₁ l₂ : LatticeT n} →
+                     FiniteHeightLattice._≈_ (FHL n) l₁ l₂ →
+                     (n , l₁) ≈ (n , l₂)
+
+        ≈-refl : ∀ {e : Elem} → e ≈ e
+        ≈-refl {n , l} = ≈-lift (FiniteHeightLattice.≈-refl (FHL n))
+
+        ≈-sym : ∀ {e₁ e₂ : Elem} → e₁ ≈ e₂ → e₂ ≈ e₁
+        ≈-sym {n₁ , l₁} (≈-lift l₁≈l₂) = ≈-lift (FiniteHeightLattice.≈-sym (FHL n₁) l₁≈l₂)
+
+        ≈-trans : ∀ {e₁ e₂ e₃ : Elem} → e₁ ≈ e₂ → e₂ ≈ e₃ → e₁ ≈ e₃
+        ≈-trans {n₁ , l₁} (≈-lift l₁≈l₂) (≈-lift l₂≈l₃) = ≈-lift (FiniteHeightLattice.≈-trans (FHL n₁) l₁≈l₂ l₂≈l₃)
+
+        _⊔_ : Elem → Elem → Elem
+        _⊔_ e₁ e₂
+            using n₁ ← proj₁ e₁ using n₂ ← proj₁ e₂
+            using n' ← n₁ ⊔ᵇ n₂ = (n' , select n' e₁ e₂)
+            where
+                select : ∀ n' e₁ e₂ → LatticeT n'
+                select n' (n₁ , l₁) (n₂ , l₂)
+                    with n' ≟ n₁ | n' ≟ n₂
+                ...   | yes refl | yes refl = FiniteHeightLattice._⊔_ (FHL n') l₁ l₂
+                ...   | yes refl | _ = l₁
+                ...   | _ | yes refl = l₂
+                ...   | no _ | no _ = FiniteHeightLattice.⊥ (FHL n')
+
+        ⊔-idemp : ∀ e → (e ⊔ e) ≈ e
+        ⊔-idemp (n , l) rewrite ⊔ᵇ-idemp n
+            with n ≟ n
+        ...   | yes refl = ≈-lift (FiniteHeightLattice.⊔-idemp (FHL n) l)
+        ...   | no n≢n = ⊥-elim (n≢n refl)
+
+        ⊔-comm : ∀ (e₁ e₂ : Elem) → (e₁ ⊔ e₂) ≈ (e₂ ⊔ e₁)
+        ⊔-comm (n₁ , l₁) (n₂ , l₂)
+            rewrite ⊔ᵇ-comm n₁ n₂
+            with n ← n₂ ⊔ᵇ n₁
+            with n ≟ n₁ | n ≟ n₂
+        ...   | yes refl | yes refl = ≈-lift (FiniteHeightLattice.⊔-comm (FHL n) l₁ l₂)
+        ...   | no _ | yes refl = ≈-lift (FiniteHeightLattice.≈-refl (FHL n))
+        ...   | yes refl | no _ = ≈-lift (FiniteHeightLattice.≈-refl (FHL n))
+        ...   | no _ | no _ = ≈-lift (FiniteHeightLattice.≈-refl (FHL n))
+
+        private
+            scary : ∀ (n₁ n₂ : Node) → (p : n₁ ≡ n₂) → (n₁ ≟ n₂) ≡ subst (λ n → Dec (n₁ ≡ n)) p (yes refl)
+            scary n₁ n₂ refl with n₁ ≟ n₂
+            ... | yes refl = refl
+            ... | no n₁≢n₂ = ⊥-elim (n₁≢n₂ refl)
+
+            payloadˡ : ∀ e₁ e₂ e₃ → let n = proj₁ ((e₁ ⊔ e₂) ⊔ e₃)
+                                    in LatticeT n
+            payloadˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                with n ← (n₁ ⊔ᵇ n₂) ⊔ᵇ n₃
+                using _⊔ⁿ_ ← FiniteHeightLattice._⊔_ (FHL n)
+                with n ≟ n₁ | n ≟ n₂ | n ≟ n₃
+            ...   | yes refl | yes refl | yes refl = (l₁ ⊔ⁿ l₂) ⊔ⁿ l₃
+            ...   | yes refl | yes refl | no _ = l₁ ⊔ⁿ l₂
+            ...   | yes refl | no _ | yes refl = l₁ ⊔ⁿ l₃
+            ...   | yes refl | no _ | no _ = l₁
+            ...   | no _ | yes refl | yes refl = l₂ ⊔ⁿ l₃
+            ...   | no _ | yes refl | no _ = l₂
+            ...   | no _ | no _ | yes refl = l₃
+            ...   | no _ | no _ | no _ = FiniteHeightLattice.⊥ (FHL n)
+
+            payloadʳ : ∀ e₁ e₂ e₃ → let n = proj₁ (e₁ ⊔ (e₂ ⊔ e₃))
+                                    in LatticeT n
+            payloadʳ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                with n ← n₁ ⊔ᵇ (n₂ ⊔ᵇ n₃)
+                using _⊔ⁿ_ ← FiniteHeightLattice._⊔_ (FHL n)
+                with n ≟ n₁ | n ≟ n₂ | n ≟ n₃
+            ...   | yes refl | yes refl | yes refl = l₁ ⊔ⁿ (l₂ ⊔ⁿ l₃)
+            ...   | yes refl | yes refl | no _ = l₁ ⊔ⁿ l₂
+            ...   | yes refl | no _ | yes refl = l₁ ⊔ⁿ l₃
+            ...   | yes refl | no _ | no _ = l₁
+            ...   | no _ | yes refl | yes refl = l₂ ⊔ⁿ l₃
+            ...   | no _ | yes refl | no _ = l₂
+            ...   | no _ | no _ | yes refl = l₃
+            ...   | no _ | no _ | no _ = FiniteHeightLattice.⊥ (FHL n)
+
+            ⊔ᵇ-prop : ∀ n₁ n₂ n₃ → (n₁ ⊔ᵇ n₂) ⊔ᵇ n₃ ≡ n₁ →
+                                   (n₁ ⊔ᵇ n₂ ≡ n₁) × (n₁ ⊔ᵇ n₃ ≡ n₁)
+            ⊔ᵇ-prop n₁ n₂ n₃ pⁿ =
+                let n₁≼n₁⊔n₂ = x≼ᵇx⊔ᵇy n₁ n₂
+                    n₁⊔n₂≼n₁₂⊔n₃ = x≼ᵇx⊔ᵇy (n₁ ⊔ᵇ n₂) n₃
+                    n₁⊔n₂≼n₁ = trans (trans (≡-⊔ᵇ-cong refl (sym pⁿ)) (n₁⊔n₂≼n₁₂⊔n₃)) pⁿ
+                    n₁⊔n₂≡n₁ = ≼ᵇ-antisym n₁⊔n₂≼n₁ n₁≼n₁⊔n₂
+                    n₁≼n₁⊔n₃ = x≼ᵇx⊔ᵇy n₁ n₃
+                    n₁⊔n₃≼n₁₂⊔n₃ = ⊔ᵇ-Monotonicʳ n₃ n₁≼n₁⊔n₂
+                    n₁⊔n₃≼n₁ = trans (trans (≡-⊔ᵇ-cong refl (sym pⁿ)) (n₁⊔n₃≼n₁₂⊔n₃)) pⁿ
+                    n₁⊔n₃≡n₁ = ≼ᵇ-antisym n₁⊔n₃≼n₁ n₁≼n₁⊔n₃
+                in (n₁⊔n₂≡n₁ , n₁⊔n₃≡n₁)
+
+            Reassocˡ : ∀ e₁ e₂ e₃ →
+                      ((e₁ ⊔ e₂) ⊔ e₃) ≈ (proj₁ ((e₁ ⊔ e₂) ⊔ e₃) , payloadˡ e₁ e₂ e₃)
+            Reassocˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                with n ← (n₁ ⊔ᵇ n₂) ⊔ᵇ n₃ in pⁿ
+                with n ≟ n₁ in d₁ | n ≟ n₂ in d₂ | n ≟ n₃ in d₃
+            Reassocˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                  | yes refl | yes refl | yes refl
+                    with (n₁ ⊔ᵇ n₁) ≟ n₁
+            ...       | no n₁≢n₁ = ⊥-elim (n₁≢n₁ (⊔ᵇ-idemp n₁))
+            ...       | yes p rewrite p
+                        with n₁ ≟ n₁
+            ...           | no n₁≢n₁ = ⊥-elim (n₁≢n₁ refl)
+            ...           | yes refl = ≈-refl
+            Reassocˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                  | yes refl | yes refl | no _
+                    with (n₁ ⊔ᵇ n₁) ≟ n₁
+            ...       | no n₁≢n₁ = ⊥-elim (n₁≢n₁ (⊔ᵇ-idemp n₁))
+            ...       | yes p rewrite p
+                        with n₁ ≟ n₁
+            ...           | no n₁≢n₁ = ⊥-elim (n₁≢n₁ refl)
+            ...           | yes refl = ≈-refl
+            Reassocˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                  | yes p₁@refl | no n₁≢n₂ | yes p₃@refl
+                    using n₁⊔n₂≡n₁ ← trans (trans (trans (≡-⊔ᵇ-cong (sym (⊔ᵇ-idemp n₁)) (refl {x = n₂})) (⊔ᵇ-assoc n₁ n₁ n₂)) (⊔ᵇ-comm n₁ (n₁ ⊔ᵇ n₂))) pⁿ
+                    with (n₁ ⊔ᵇ n₂) ≟ n₁
+            ...       | no n₁⊔n₂≢n₁ = ⊥-elim (n₁⊔n₂≢n₁ n₁⊔n₂≡n₁)
+            ...       | yes p rewrite p
+                        with n₁ ≟ n₁ | n₁ ≟ n₂
+            ...           | no n₁≢n₁ | _ = ⊥-elim (n₁≢n₁ refl)
+            ...           | _ | yes n₁≡n₂ = ⊥-elim (n₁≢n₂ n₁≡n₂)
+            ...           | yes refl | no _ = ≈-refl
+            Reassocˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                  | yes p₁@refl | no n₁≢n₂ | no n₁≢n₃
+                    using (n₁⊔n₂≡n₁ , n₁⊔n₃≡n₁) ← ⊔ᵇ-prop n₁ n₂ n₃ pⁿ
+                    with n₁ ⊔ᵇ n₂ ≟ n₁
+            ...       | no n₁⊔n₂≢n₁ = ⊥-elim (n₁⊔n₂≢n₁ n₁⊔n₂≡n₁)
+            ...       | yes p rewrite p
+                        with n₁ ≟ n₁ | n₁ ≟ n₂
+            ...           | no n₁≢n₁ | _ = ⊥-elim (n₁≢n₁ refl)
+            ...           | _ | yes n₁≡n₂ = ⊥-elim (n₁≢n₂ n₁≡n₂)
+            ...           | yes refl | no _ = ≈-refl
+            Reassocˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                  | no n₂≢n₁ | yes p₂@refl | yes p₃@refl
+                    using n₁⊔n₂≡n₂ ← trans (trans (≡-⊔ᵇ-cong (refl {x = n₁}) (sym (⊔ᵇ-idemp n₂))) (sym (⊔ᵇ-assoc n₁ n₂ n₂))) pⁿ
+                    with (n₁ ⊔ᵇ n₂) ≟ n₂
+            ...       | no n₁⊔n₂≢n₂ = ⊥-elim (n₁⊔n₂≢n₂ n₁⊔n₂≡n₂)
+            ...       | yes p rewrite p
+                        with n₂ ≟ n₁ | n₂ ≟ n₂
+            ...           | yes n₂≡n₁ | _ = ⊥-elim (n₂≢n₁ n₂≡n₁)
+            ...           | _ | no n₂≢n₂ = ⊥-elim (n₂≢n₂ refl)
+            ...           | no _ | yes refl = ≈-refl
+            Reassocˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                  | no n₂≢n₁ | yes p₂@refl | no n₂≢n₃
+                    using (n₂⊔n₁≡n₂ , n₂⊔n₃≡n₂) ← ⊔ᵇ-prop n₂ n₁ n₃ (trans (≡-⊔ᵇ-cong (⊔ᵇ-comm n₂ n₁) (refl {x = n₃})) pⁿ)
+                    with (n₁ ⊔ᵇ n₂) ≟ n₁ | (n₁ ⊔ᵇ n₂) ≟ n₂
+            ...       | yes n₁⊔n₂≡n₁ | _ = ⊥-elim (n₂≢n₁ (trans (sym n₂⊔n₁≡n₂) (trans (⊔ᵇ-comm n₂ n₁) (n₁⊔n₂≡n₁))))
+            ...       | _ | no n₁⊔n₂≢n₂ = ⊥-elim (n₁⊔n₂≢n₂ (trans (⊔ᵇ-comm n₁ n₂) n₂⊔n₁≡n₂))
+            ...       | no n₁⊔n₂≢n₁ | yes p rewrite p
+                        with n₂ ≟ n₂
+            ...           | no n₂≢n₂ = ⊥-elim (n₂≢n₂ refl)
+            ...           | yes refl = ≈-refl
+            Reassocˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                  | no n₃≢n₁ | no n₃≢n₂ | yes p₃@refl
+                    with n₁₂ ← n₁ ⊔ᵇ n₂
+                    with n₃ ≟ n₁₂
+            ...       | no n₃≢n₁₂ = ≈-refl
+            ...       | yes refl rewrite d₁ rewrite d₂ = ≈-lift (⊥≼x l₃) -- TODO: need ⊥ ⊔ n₃ ≡ n₃
+            Reassocˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                  | no n≢n₁ | no n≢n₂ | no n≢n₃
+                    with n₁₂ ← n₁ ⊔ᵇ n₂
+                    with n₁₂ ≟ n₁ | n₁₂ ≟ n₂ | n ≟ n₃ | n ≟ n₁₂
+            ...       | _ | _ | yes n≡n₃ | _ = ⊥-elim (n≢n₃ n≡n₃)
+            ...       | _ | _ | no _ | no n≢n₁₂ = ≈-refl
+            ...       | yes refl | yes refl | no _ | yes refl = ⊥-elim (n≢n₁ refl)
+            ...       | yes refl | no n₁₂≢n₂ | no _ | yes refl = ⊥-elim (n≢n₁ refl)
+            ...       | no n₁₂≢n₁ | yes refl | no _ | yes refl = ⊥-elim (n≢n₂ refl)
+            ...       | no _ | no _ | no _ | yes refl = ≈-refl
+
+            Reassocʳ : ∀ e₁ e₂ e₃ →
+                       (e₁ ⊔ (e₂ ⊔ e₃)) ≈ (proj₁ (e₁ ⊔ (e₂ ⊔ e₃)) , payloadʳ e₁ e₂ e₃)
+            Reassocʳ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                with n ← n₁ ⊔ᵇ (n₂ ⊔ᵇ n₃) in pⁿ
+                with n ≟ n₁ in d₁ | n ≟ n₂ in d₂ | n ≟ n₃ in d₃
+            Reassocʳ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                  | yes refl | yes refl | yes refl
+                    with (n₁ ⊔ᵇ n₁) ≟ n₁
+            ...       | no n₁≢n₁ = ⊥-elim (n₁≢n₁ (⊔ᵇ-idemp n₁))
+            ...       | yes p rewrite p
+                        with n₁ ≟ n₁
+            ...           | no n₁≢n₁ = ⊥-elim (n₁≢n₁ refl)
+            ...           | yes refl = ≈-refl
+            Reassocʳ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                  | yes refl | yes refl | no n₁≢n₃
+                    using n₁⊔n₃≡n₁ ← trans (≡-⊔ᵇ-cong (sym (⊔ᵇ-idemp n₁)) (refl {x = n₃})) (trans (⊔ᵇ-assoc n₁ n₁ n₃) pⁿ)
+                    rewrite n₁⊔n₃≡n₁
+                    with n₁ ≟ n₁ | n₁ ≟ n₃
+            ...     | no n₁≢n₁ | _ = ⊥-elim (n₁≢n₁ refl)
+            ...     | _ | yes n₁≡n₃ = ⊥-elim (n₁≢n₃ n₁≡n₃)
+            ...     | yes refl | no _ = ≈-refl
+            Reassocʳ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                  | yes refl | no n₁≢n₂ | yes refl
+                    using n₂⊔n₁≡n₁ ← trans (trans (trans (≡-⊔ᵇ-cong (refl {x = n₂}) (sym (⊔ᵇ-idemp n₁))) (sym (⊔ᵇ-assoc n₂ n₁ n₁))) (⊔ᵇ-comm _ _)) pⁿ
+                    rewrite n₂⊔n₁≡n₁
+                    with n₁ ≟ n₁ | n₁ ≟ n₂
+            ...       | no n₁≢n₁ | _ = ⊥-elim (n₁≢n₁ refl)
+            ...       | _ | yes n₁≡n₂ = ⊥-elim (n₁≢n₂ n₁≡n₂)
+            ...       | yes refl | no _ = ≈-refl
+            Reassocʳ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                  | yes refl | no n₁≢n₂ | no n₁≢n₃
+                    with n₂₃ ← n₂ ⊔ᵇ n₃
+                    with n₁ ≟ n₂₃
+            ...       | no n₁≢n₂₃ = ≈-refl
+            ...       | yes refl rewrite d₂ rewrite d₃ = ≈-lift (FiniteHeightLattice.≈-trans (FHL n₁) (FiniteHeightLattice.⊔-comm (FHL n₁) _ _) (⊥≼x l₁))
+            Reassocʳ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                  | no n₂≢n₁ | yes refl | yes refl
+                    rewrite ⊔ᵇ-idemp n₂
+                    with n₂ ≟ n₂
+            ...       | no n₂≢n₂ = ⊥-elim (n₂≢n₂ refl)
+            ...       | yes refl = ≈-refl
+            Reassocʳ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                  | no n₂≢n₁ | yes refl | no n₂≢n₃
+                  using (n₂⊔n₃=n₂ , n₂⊔n₁=n₂) ← ⊔ᵇ-prop n₂ n₃ n₁ (trans (⊔ᵇ-comm _ _) pⁿ)
+                  rewrite n₂⊔n₃=n₂
+                  with n₂ ≟ n₂ | n₂ ≟ n₃
+            ...     | no n₂≢n₂ | _ = ⊥-elim (n₂≢n₂ refl)
+            ...     | _ | yes n₂≡n₃ = ⊥-elim (n₂≢n₃ n₂≡n₃)
+            ...     | yes refl | no _ = ≈-refl
+            Reassocʳ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                  | no n₃≢n₁ | no n₃≢n₂ | yes refl
+                    using (n₃⊔n₂≡n₃ , n₃⊔n₁≡n₃) ← ⊔ᵇ-prop n₃ n₂ n₁ (trans (⊔ᵇ-comm _ _) (trans (≡-⊔ᵇ-cong (refl {x = n₁}) (⊔ᵇ-comm n₃ n₂)) pⁿ))
+                    rewrite trans (⊔ᵇ-comm _ _) n₃⊔n₂≡n₃
+                    with n₃ ≟ n₃ | n₃ ≟ n₂
+            ...       | no n₃≢n₃ | _ = ⊥-elim (n₃≢n₃ refl)
+            ...       | _ | yes n₃≡n₂ = ⊥-elim (n₃≢n₂ n₃≡n₂)
+            ...       | yes refl | no _ = ≈-refl
+            Reassocʳ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                  | no n≢n₁ | no n≢n₂ | no n≢n₃
+                    with n₂₃ ← n₂ ⊔ᵇ n₃
+                    with n₂₃ ≟ n₂ | n₂₃ ≟ n₃ | n ≟ n₁ | n ≟ n₂₃
+            ...       | _ | _ | yes n≡n₁ | _ = ⊥-elim (n≢n₁ n≡n₁)
+            ...       | _ | _ | no _ | no _ = ≈-refl
+            ...       | yes refl | yes refl | no _ | yes refl = ⊥-elim (n≢n₂ refl)
+            ...       | yes refl | no n₁₂≢n₂ | no _ | yes refl = ⊥-elim (n≢n₂ refl)
+            ...       | no n₁₂≢n₁ | yes refl | no _ | yes refl = ⊥-elim (n≢n₃ refl)
+            ...       | no n₁₂≢n₁ | no n₁₂≢n₂ | no _ | yes refl = ≈-refl
+
+
+        ⊔-assoc : ∀ (e₁ e₂ e₃ : Elem) → ((e₁ ⊔ e₂) ⊔ e₃) ≈ (e₁ ⊔ (e₂ ⊔ e₃))
+        ⊔-assoc e₁@(n₁ , l₁) e₂@(n₂ , l₂) e₃@(n₃ , l₃)
+            with nˡ ← proj₁ ((e₁ ⊔ e₂) ⊔ e₃) in pˡ
+            with nʳ ← proj₁ (e₁ ⊔ (e₂ ⊔ e₃)) in pʳ
+            with final₁ ← Reassocˡ e₁ e₂ e₃
+            with final₂ ← Reassocʳ e₁ e₂ e₃
+            rewrite pˡ rewrite pʳ
+            rewrite ⊔ᵇ-assoc n₁ n₂ n₃
+            rewrite trans (sym pˡ ) pʳ
+            with nʳ ≟ n₁ | nʳ ≟ n₂ | nʳ ≟ n₃
+        ...   | yes refl | yes refl | yes refl =
+            let l-assoc = FiniteHeightLattice.⊔-assoc (FHL n₁) l₁ l₂ l₃
+            in ≈-trans final₁ (≈-trans (≈-lift l-assoc) (≈-sym final₂))
+        ...   | yes refl | yes refl | no _ = ≈-trans final₁ (≈-sym final₂)
+        ...   | yes refl | no _ | yes refl = ≈-trans final₁ (≈-sym final₂)
+        ...   | yes refl | no _ | no _ = ≈-trans final₁ (≈-sym final₂)
+        ...   | no _ | yes refl | yes refl = ≈-trans final₁ (≈-sym final₂)
+        ...   | no _ | yes refl | no _ = ≈-trans final₁ (≈-sym final₂)
+        ...   | no _ | no _ | yes refl = ≈-trans final₁ (≈-sym final₂)
+        ...   | no _ | no _ | no _ = ≈-trans final₁ (≈-sym final₂)