Move proof of least element into FiniteHeightLattice

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

Analysis/Forward.agda

@@ -21,7 +21,7 @@ open IsFiniteHeightLattice isFiniteHeightLatticeˡ
     using () renaming (isLattice to isLatticeˡ)
 
 module WithProg (prog : Program) where
-    open import Analysis.Forward.Lattices L prog hiding (≈ᵛ-Decidable) -- to disambiguate instance resolution
+    open import Analysis.Forward.Lattices L prog hiding (≈ᵛ-Decidable; ≈ᵐ-Decidable) -- to disambiguate instance resolution
     open import Analysis.Forward.Evaluation L prog
     open Program prog
 
@@ -66,7 +66,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 ≈ᵐ-Decidable isFiniteHeightLatticeᵐ analyze (λ {m₁} {m₂} m₁≼m₂ → analyze-Mono {m₁} {m₂} m₁≼m₂)
+        open import Fixedpoint analyze (λ {m₁} {m₂} m₁≼m₂ → analyze-Mono {m₁} {m₂} m₁≼m₂)
             using ()
             renaming (aᶠ to result; aᶠ≈faᶠ to result≈analyze-result)
             public

Fixedpoint.agda

@@ -5,8 +5,8 @@ module Fixedpoint {a} {A : Set a}
                   {h : ℕ}
                   {_≈_ : A → A → Set a}
                   {_⊔_ : A → A → A} {_⊓_ : A → A → A}
-                  (≈-Decidable : IsDecidable _≈_)
+                  {{ ≈-Decidable : IsDecidable _≈_ }}
-                  (flA : IsFiniteHeightLattice A h _≈_ _⊔_ _⊓_)
+                  {{flA : IsFiniteHeightLattice A h _≈_ _⊔_ _⊓_}}
                   (f : A → A)
                   (Monotonicᶠ : Monotonic (IsFiniteHeightLattice._≼_ flA)
                                           (IsFiniteHeightLattice._≼_ flA) f) where
@@ -28,24 +28,9 @@ private
         using ()
         renaming
             ( ⊥ to ⊥ᴬ
-            ; longestChain to longestChainᴬ
             ; bounded to boundedᴬ
             )
 
-
-    ⊥ᴬ≼ : ∀ (a : A) → ⊥ᴬ ≼ a
-    ⊥ᴬ≼ a with ≈-dec a ⊥ᴬ
-    ...   | yes a≈⊥ᴬ = ≼-cong a≈⊥ᴬ ≈-refl (≼-refl a)
-    ...   | no a̷≈⊥ᴬ with ≈-dec ⊥ᴬ (a ⊓ ⊥ᴬ)
-    ...         | yes ⊥ᴬ≈a⊓⊥ᴬ = ≈-trans (⊔-comm ⊥ᴬ a) (≈-trans (≈-⊔-cong (≈-refl {a}) ⊥ᴬ≈a⊓⊥ᴬ) (absorb-⊔-⊓ a ⊥ᴬ))
-    ...         | no ⊥ᴬ̷≈a⊓⊥ᴬ = ⊥-elim (ChainA.Bounded-suc-n boundedᴬ (ChainA.step x≺⊥ᴬ ≈-refl longestChainᴬ))
-                    where
-                        ⊥ᴬ⊓a̷≈⊥ᴬ : ¬ (⊥ᴬ ⊓ a) ≈ ⊥ᴬ
-                        ⊥ᴬ⊓a̷≈⊥ᴬ = λ ⊥ᴬ⊓a≈⊥ᴬ → ⊥ᴬ̷≈a⊓⊥ᴬ (≈-trans (≈-sym ⊥ᴬ⊓a≈⊥ᴬ) (⊓-comm _ _))
-
-                        x≺⊥ᴬ : (⊥ᴬ ⊓ a) ≺ ⊥ᴬ
-                        x≺⊥ᴬ = (≈-trans (⊔-comm _ _) (≈-trans (≈-refl {⊥ᴬ ⊔ (⊥ᴬ ⊓ a)}) (absorb-⊔-⊓ ⊥ᴬ a)) , ⊥ᴬ⊓a̷≈⊥ᴬ)
-
     -- using 'g', for gas, here helps make sure the function terminates.
     -- since A forms a fixed-height lattice, we must find a solution after
     -- 'h' steps at most. Gas is set up such that as soon as it runs
@@ -65,7 +50,7 @@ private
                     c' rewrite +-comm 1 hᶜ = ChainA.concat c (ChainA.step a₂≺fa₂ ≈-refl (ChainA.done (≈-refl {f a₂})))
 
     fix : Σ A (λ a → a ≈ f a)
-    fix = doStep (suc h) 0 ⊥ᴬ ⊥ᴬ (ChainA.done ≈-refl) (+-comm (suc h) 0) (⊥ᴬ≼ (f ⊥ᴬ))
+    fix = doStep (suc h) 0 ⊥ᴬ ⊥ᴬ (ChainA.done ≈-refl) (+-comm (suc h) 0) (⊥≼ (f ⊥ᴬ))
 
 aᶠ : A
 aᶠ = proj₁ fix
@@ -85,4 +70,4 @@ private
     ...   | no  _ = stepPreservesLess g' _ _ _ b b≈fb (≼-cong ≈-refl (≈-sym b≈fb) (Monotonicᶠ a₂≼b)) _ _ _
 
 aᶠ≼ : ∀ (a : A) → a ≈ f a → aᶠ ≼ a
-aᶠ≼ a a≈fa = stepPreservesLess (suc h) 0 ⊥ᴬ ⊥ᴬ a a≈fa (⊥ᴬ≼ a) (ChainA.done ≈-refl) (+-comm (suc h) 0) (⊥ᴬ≼ (f ⊥ᴬ))
+aᶠ≼ a a≈fa = stepPreservesLess (suc h) 0 ⊥ᴬ ⊥ᴬ a a≈fa (⊥≼ a) (ChainA.done ≈-refl) (+-comm (suc h) 0) (⊥≼ (f ⊥ᴬ))

Isomorphism.agda

@@ -68,6 +68,7 @@ module TransportFiniteHeight
         renaming (⊥ to ⊥₁; ⊤ to ⊤₁; bounded to bounded₁; longestChain to c)
 
     instance
+        fixedHeight : IsLattice.FixedHeight lB height
         fixedHeight = record
             { ⊥ = f ⊥₁
             ; ⊤ = f ⊤₁

Lattice.agda

@@ -4,7 +4,8 @@ open import Equivalence
 import Chain
 
 open import Relation.Binary.Core using (_Preserves_⟶_ )
-open import Relation.Nullary using (Dec; ¬_)
+open import Relation.Nullary using (Dec; ¬_; yes; no)
+open import Data.Empty using (⊥-elim)
 open import Data.Nat as Nat using (ℕ)
 open import Data.Product using (_×_; Σ; _,_)
 open import Data.Sum using (_⊎_; inj₁; inj₂)
@@ -236,6 +237,28 @@ record IsFiniteHeightLattice {a} (A : Set a)
     field
         {{fixedHeight}} : FixedHeight h
 
+    -- 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
+        ⊥≼ a with ≈-dec a ⊥
+        ...   | yes a≈⊥ = ≼-cong a≈⊥ ≈-refl (≼-refl a)
+        ...   | no a̷≈⊥ with ≈-dec ⊥ (a ⊓ ⊥)
+        ...         | yes ⊥≈a⊓⊥ = ≈-trans (⊔-comm ⊥ a) (≈-trans (≈-⊔-cong (≈-refl {a}) ⊥≈a⊓⊥) (absorb-⊔-⊓ a ⊥))
+        ...         | no ⊥ᴬ̷≈a⊓⊥ = ⊥-elim (MyChain.Bounded-suc-n bounded (MyChain.step x≺⊥ ≈-refl longestChain))
+                        where
+                            ⊥⊓a̷≈⊥ : ¬ (⊥ ⊓ a) ≈ ⊥
+                            ⊥⊓a̷≈⊥ = λ ⊥⊓a≈⊥ → ⊥ᴬ̷≈a⊓⊥ (≈-trans (≈-sym ⊥⊓a≈⊥) (⊓-comm _ _))
+
+                            x≺⊥ : (⊥ ⊓ a) ≺ ⊥
+                            x≺⊥ = (≈-trans (⊔-comm _ _) (≈-trans (≈-refl {⊥ ⊔ (⊥ ⊓ a)}) (absorb-⊔-⊓ ⊥ a)) , ⊥⊓a̷≈⊥)
+
 module ChainMapping {a b} {A : Set a} {B : Set b}
     {_≈₁_ : A → A → Set a} {_≈₂_ : B → B → Set b}
     {_⊔₁_ : A → A → A} {_⊔₂_ : B → B → B}

Lattice/Builder.agda

@@ -72,7 +72,7 @@ record IsPartialSemilattice {a} {A : Set a}
     _≼_ x y = (x ⊔? y) ≈? (just y)
 
     field
-        ≈-equiv : IsEquivalence A _≈_
+        {{≈-equiv}} : IsEquivalence A _≈_
         ≈-⊔-cong : PartialCong _≈_ _⊔?_
 
         ⊔-assoc : PartialAssoc _≈_ _⊔?_
@@ -148,6 +148,10 @@ record IsPartialSemilattice {a} {A : Set a}
                 with a₁ ⊔? x | refl⇒a₁⊔?x=nothing refl | x-absorbʳ a₁
         ...       | nothing | refl | ()
 
+
+PartialAbsorb : ∀ {a} {A : Set a} (_≈_ : A → A → Set a) (_⊗₁_ : A → A → Maybe A) (_⊗₂_ : A → A → Maybe A) → Set a
+PartialAbsorb {a} {A} _≈_ _⊗₁_ _⊗₂_ = ∀ (x y : A) →  maybe (λ x⊗₂y → lift-≈ _≈_ (x ⊗₁ x⊗₂y) (just x)) (Trivial _) (x ⊗₂ y)
+
 record IsPartialLattice {a} {A : Set a}
     (_≈_ : A → A → Set a)
     (_⊔?_ : A → A → Maybe A)
@@ -157,8 +161,8 @@ record IsPartialLattice {a} {A : Set a}
         {{partialJoinSemilattice}} : IsPartialSemilattice _≈_ _⊔?_
         {{partialMeetSemilattice}} : IsPartialSemilattice _≈_ _⊓?_
 
-        absorb-⊔-⊓ : (x y : A) →  maybe (λ x⊓y → lift-≈ _≈_ (x ⊔? x⊓y) (just x)) (Trivial _) (x ⊓? y)
+        absorb-⊔-⊓ : PartialAbsorb _≈_ _⊔?_ _⊓?_
-        absorb-⊓-⊔ : (x y : A) →  maybe (λ x⊔y → lift-≈ _≈_ (x ⊓? x⊔y) (just x)) (Trivial _) (x ⊔? y)
+        absorb-⊓-⊔ : PartialAbsorb _≈_ _⊓?_ _⊔?_
 
     open IsPartialSemilattice partialJoinSemilattice
         renaming (HasAbsorbingElement to HasGreatestElement)
@@ -213,6 +217,7 @@ record PartialLattice {a} (A : Set a) : Set (lsuc a) where
     least-⊔-identˡ le x = ≈?-trans (⊔-comm (HasLeastElement.x le) x) (least-⊔-identʳ le x)
 
 record PartialLatticeType (a : Level) : Set (lsuc a) where
+    constructor mkPartialLatticeType
     field
         EltType : Set a
         {{partialLattice}} : PartialLattice EltType
@@ -304,6 +309,12 @@ pathJoin' (add-via-greatest l ls) (inj₁ lv₁) (inj₂ p₂) = just (inj₁ lv
 pathJoin' (add-via-greatest l ls) (inj₂ p₁) (inj₁ lv₂) = just (inj₁ lv₂)
 pathJoin' (add-via-greatest l ls {{greatest}}) (inj₂ p₁) (inj₂ p₂) = Maybe.map inj₂ (pathJoin' ls p₁ p₂) -- not our job to provide the least element here. If there was a "greatest" there, recursion would've found it (?)
 
+greatestPath : ∀ {a} (Ls : Layers a) (greatest : LayerGreatest (head Ls)) → Path' Ls
+greatestPath Ls greatest
+    with head Ls | greatest | valueAtHead Ls
+...   | _ | MkLayerGreatest {{hasGreatest = hasGreatest}} | vah
+      = vah (inj₁ (IsPartialSemilattice.HasAbsorbingElement.x hasGreatest))
+
 pathMeet' : ∀ {a} (Ls : Layers a) (p₁ p₂ : Path' Ls) →  Maybe (Path' Ls)
 pathMeet' (single l) lv₁ lv₂ = lvMeet (toList l) lv₁ lv₂
 pathMeet' (add-via-least l ls) (inj₁ lv₁) (inj₁ lv₂) = Maybe.map inj₁ (lvMeet (toList l) lv₁ lv₂)
@@ -313,10 +324,7 @@ pathMeet' (add-via-least l ls) (inj₂ p₁) (inj₂ p₂) = Maybe.map inj₂ (p
 pathMeet' (add-via-greatest l ls {{greatest}}) (inj₁ lv₁) (inj₁ lv₂)
     with lvMeet (toList l) lv₁ lv₂
 ...   | just lv = just (inj₁ lv)
-...   | nothing
+...   | nothing = just (inj₂ (greatestPath ls greatest))
-        with head ls | greatest | valueAtHead ls
-...       | _ | MkLayerGreatest {{hasGreatest = hasGreatest}} | vah
-          = just (inj₂ (vah (inj₁ (IsPartialSemilattice.HasAbsorbingElement.x hasGreatest))))
 pathMeet' (add-via-greatest l ls) (inj₁ lv₁) (inj₂ p₂) = just (inj₂ p₂)
 pathMeet' (add-via-greatest l ls) (inj₂ p₁) (inj₁ lv₂) = just (inj₂ p₁)
 pathMeet' (add-via-greatest l ls) (inj₂ p₁) (inj₂ p₂) = Maybe.map inj₂ (pathMeet' ls p₁ p₂)
@@ -462,6 +470,29 @@ eqPath'-pathJoin'-cong {Ls = add-via-greatest l ls {{greatest}}} {inj₂ p₁} {
 ...   | just p₁⊔p₃ | just p₂⊔p₄ | ≈-just p₁⊔p₃≈p₂⊔p₄ = ≈-just p₁⊔p₃≈p₂⊔p₄
 ...   | nothing | nothing | ≈-nothing = ≈-nothing
 
+eqPath'-pathMeet'-cong : ∀ {a} {Ls : Layers a} {a₁ a₂ a₃ a₄} →  eqPath' Ls a₁ a₂ →  eqPath' Ls a₃ a₄ →  lift-≈ (eqPath' Ls) (pathMeet' Ls a₁ a₃) (pathMeet' Ls a₂ a₄)
+eqPath'-pathMeet'-cong {Ls = single l} {lv₁} {lv₂} {lv₃} {lv₄} lv₁≈lv₂ lv₃≈lv₄ = eqLv-lvMeet-cong l {lv₁} {lv₂} {lv₃} {lv₄} lv₁≈lv₂ lv₃≈lv₄
+eqPath'-pathMeet'-cong {Ls = add-via-least l ls} {inj₁ lv₁} {inj₁ lv₂} {inj₁ lv₃} {inj₁ lv₄} lv₁≈lv₂ lv₃≈lv₄
+    with lvMeet (toList l) lv₁ lv₃ | lvMeet (toList l) lv₂ lv₄ | eqLv-lvMeet-cong l {lv₁} {lv₂} {lv₃} {lv₄} lv₁≈lv₂ lv₃≈lv₄
+...   | just _ | just _ | ≈-just lv₁⊓lv₃≈lv₂⊓lv₄ = ≈-just lv₁⊓lv₃≈lv₂⊓lv₄
+...   | nothing | nothing | ≈-nothing = ≈-nothing
+eqPath'-pathMeet'-cong {Ls = add-via-least l ls} {inj₂ p₁} {inj₂ p₂} {inj₁ lv₃} {inj₁ lv₄} p₁≈p₂ lv₃≈lv₄ = ≈-just p₁≈p₂
+eqPath'-pathMeet'-cong {Ls = add-via-least l ls} {inj₁ lv₁} {inj₁ lv₂} {inj₂ p₃} {inj₂ p₄} lv₁≈lv₂ p₃≈p₄ = ≈-just p₃≈p₄
+eqPath'-pathMeet'-cong {Ls = add-via-least l {{least}}  ls} {inj₂ p₁} {inj₂ p₂} {inj₂ p₃} {inj₂ p₄} p₁≈p₂ p₃≈p₄
+    with pathMeet' ls p₁ p₃ | pathMeet' ls p₂ p₄ | eqPath'-pathMeet'-cong {Ls = ls} {p₁} {p₂} {p₃} {p₄} p₁≈p₂ p₃≈p₄
+...   | just p₁⊓p₃ | just p₂⊓p₄ | ≈-just p₁⊓p₃≈p₂⊓p₄ = ≈-just p₁⊓p₃≈p₂⊓p₄
+...   | nothing | nothing | ≈-nothing = ≈-nothing
+eqPath'-pathMeet'-cong {Ls = add-via-greatest l ls {{greatest}}} {inj₁ lv₁} {inj₁ lv₂} {inj₁ lv₃} {inj₁ lv₄} lv₁≈lv₂ lv₃≈lv₄
+    with lvMeet (toList l) lv₁ lv₃ | lvMeet (toList l) lv₂ lv₄ | eqLv-lvMeet-cong l {lv₁} {lv₂} {lv₃} {lv₄} lv₁≈lv₂ lv₃≈lv₄
+...   | just _ | just _ | ≈-just lv₁⊓lv₃≈lv₂⊓lv₄ = ≈-just lv₁⊓lv₃≈lv₂⊓lv₄
+...   | nothing | nothing | ≈-nothing = ≈-just (eqPath'-refl ls (greatestPath ls greatest))
+eqPath'-pathMeet'-cong {Ls = add-via-greatest l ls} {inj₂ p₁} {inj₂ p₂} {inj₁ lv₃} {inj₁ lv₄} p₁≈p₂ lv₃≈lv₄ = ≈-just p₁≈p₂
+eqPath'-pathMeet'-cong {Ls = add-via-greatest l ls} {inj₁ lv₁} {inj₁ lv₂} {inj₂ p₃} {inj₂ p₄} lv₁≈lv₂ p₃≈p₄ = ≈-just p₃≈p₄
+eqPath'-pathMeet'-cong {Ls = add-via-greatest l ls {{greatest}}} {inj₂ p₁} {inj₂ p₂} {inj₂ p₃} {inj₂ p₄} p₁≈p₂ p₃≈p₄
+    with pathMeet' ls p₁ p₃ | pathMeet' ls p₂ p₄ | eqPath'-pathMeet'-cong {Ls = ls} {p₁} {p₂} {p₃} {p₄} p₁≈p₂ p₃≈p₄
+...   | just p₁⊓p₃ | just p₂⊓p₄ | ≈-just p₁⊓p₃≈p₂⊓p₄ = ≈-just p₁⊓p₃≈p₂⊓p₄
+...   | nothing | nothing | ≈-nothing = ≈-nothing
+
 -- Now that we can compare paths for "equality", we can state and
 -- prove theorems such as commutativity and idempotence.
 
@@ -482,6 +513,24 @@ eval _⊔?_ (e₁ ∨ e₂) = (eval _⊔?_ e₁) >>= (λ v₁ →  (eval _⊔?_
 PartiallySubHomo : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) (_⊕_ : A → A → Maybe A) (_⊗_ : B → B → Maybe B) → Set (a ⊔ℓ b)
 PartiallySubHomo {A = A} f _⊕_ _⊗_ = ∀ (a₁ a₂ : A) →  (f a₁ ⊗ f a₂) ≡ Maybe.map f (a₁ ⊕ a₂)
 
+PartialAbsorb-map : ∀ {a b} {A : Set a} {B : Set b}
+                      (f : A → B)
+                      (_≈ᵃ_ : A → A → Set a) (_≈ᵇ_ : B → B → Set b) →
+                      (∀ a₁ a₂ → a₁ ≈ᵃ a₂ → f a₁ ≈ᵇ f a₂) →
+                    ∀ (_⊕₁_ : A → A → Maybe A) (_⊕₂_ : A → A → Maybe A)
+                      (_⊗₁_ : B → B → Maybe B) (_⊗₂_ : B → B → Maybe B) →
+                      PartiallySubHomo f _⊕₁_ _⊗₁_ →
+                      PartiallySubHomo f _⊕₂_ _⊗₂_ →
+                      PartialAbsorb _≈ᵃ_ _⊕₁_ _⊕₂_ →
+                      ∀ (x y : A) →  maybe (λ x⊗₂y → lift-≈ _≈ᵇ_ (f x ⊗₁ x⊗₂y) (just (f x))) (Trivial _) (f x ⊗₂ f y)
+PartialAbsorb-map f _≈ᵃ_ _≈ᵇ_ ≈ᵃ⇒≈ᵇ _⊕₁_ _⊕₂_ _⊗₁_ _⊗₂_ psh₁ psh₂ absorbᵃ x y
+    with x ⊕₂ y | f x ⊗₂ f y | psh₂ x y | absorbᵃ x y
+...   | nothing | nothing | refl | _ = mkTrivial
+...   | just x⊕₂y | just fx⊗₂fy | refl | x⊕₁xy≈?x
+        with x ⊕₁ x⊕₂y | f x ⊗₁ (f x⊕₂y) | psh₁ x x⊕₂y | x⊕₁xy≈?x
+...       |  just x⊕₁xy | just fx⊗₁fx⊕₂y | refl | ≈-just x⊕₁xy≈x = ≈-just (≈ᵃ⇒≈ᵇ _ _ x⊕₁xy≈x)
+
+
 -- this evaluation property, which depends on PartiallySubHomo, effectively makes
 -- it easier to talk about compound operations and the preservation of their
 -- structure when _⊗_ is PartiallySubHomo.
@@ -514,6 +563,9 @@ pathJoin'-homo-greatest₁ l ls greatest e = eval-subHomo inj₁ (lvJoin (toList
 pathJoin'-homo-greatest₂ : ∀ {a} (l : Layer a) (ls : Layers a) greatest (e : Expr (Path' ls)) → eval (pathJoin' (add-via-greatest l ls {{greatest}})) (map inj₂ e) ≡ Maybe.map inj₂ (eval (pathJoin' ls) e)
 pathJoin'-homo-greatest₂ l ls greatest e = eval-subHomo inj₂ (pathJoin' ls) (pathJoin' (add-via-greatest l ls {{greatest}})) e (λ a₁ a₂ → refl)
 
+pathMeet'-homo-least₁ : ∀ {a} (l : Layer a) (ls : Layers a) least (e : Expr (LayerValue l)) → eval (pathMeet' (add-via-least l {{least}} ls)) (map inj₁ e) ≡ Maybe.map inj₁ (eval (lvMeet (toList l)) e)
+pathMeet'-homo-least₁ l ls least e = eval-subHomo inj₁ (lvMeet (toList l)) (pathMeet' (add-via-least l {{least}} ls)) e (λ a₁ a₂ → refl)
+
 lvCombine-assoc : ∀ {a} (f : CombineForPLT a) →
                   (∀ plt →  PartialAssoc (PartialLatticeType._≈_ plt) (f plt)) →
                   ∀ (L : List (PartialLatticeType a)) →
@@ -580,6 +632,30 @@ lvMeet-comm = lvCombine-comm PartialLatticeType._⊓?_ PartialLatticeType.⊓-co
 lvMeet-idemp : ∀ {a} (L : List (PartialLatticeType a)) → PartialIdemp (eqL L) (lvMeet L)
 lvMeet-idemp = lvCombine-idemp PartialLatticeType._⊓?_ PartialLatticeType.⊓-idemp
 
+lvCombine-absorb : ∀ {a} (f₁ f₂ : CombineForPLT a) →
+                   (∀ plt →  PartialAbsorb (PartialLatticeType._≈_ plt) (f₁ plt) (f₂ plt)) →
+                   ∀ (L : List (PartialLatticeType a)) →
+                   PartialAbsorb (eqL L) (lvCombine f₁ L) (lvCombine f₂ L)
+lvCombine-absorb f₁ f₂ absorb-f₁-f₂ [] ()
+lvCombine-absorb f₁ f₂ absorb-f₁-f₂ (plt ∷ plts) (inj₁ v₁) (inj₁ v₂)
+    = PartialAbsorb-map inj₁ _ _ (λ _ _ x → x) (f₁ plt) (f₂ plt)
+                                 (lvCombine f₁ (plt ∷ plts)) (lvCombine f₂ (plt ∷ plts))
+                                 (λ _ _ → refl) (λ _ _ → refl)
+                                 (absorb-f₁-f₂ plt) v₁ v₂
+lvCombine-absorb f₁ f₂ absorb-f₁-f₂ (plt ∷ plts) (inj₂ lv₁) (inj₁ v₂) = mkTrivial
+lvCombine-absorb f₁ f₂ absorb-f₁-f₂ (plt ∷ plts) (inj₁ v₁) (inj₂ lv₂) = mkTrivial
+lvCombine-absorb f₁ f₂ absorb-f₁-f₂ (plt ∷ plts) (inj₂ lv₁) (inj₂ lv₂)
+    = PartialAbsorb-map inj₂ _ _ (λ _ _ x → x) (lvCombine f₁ plts) (lvCombine f₂ plts)
+                                 (lvCombine f₁ (plt ∷ plts)) (lvCombine f₂ (plt ∷ plts))
+                                 (λ _ _ → refl) (λ _ _ → refl)
+                                 (lvCombine-absorb f₁ f₂  absorb-f₁-f₂ plts) lv₁ lv₂
+
+absorb-lvJoin-lvMeet : ∀ {a} (L : List (PartialLatticeType a)) → PartialAbsorb (eqL L) (lvJoin L) (lvMeet L)
+absorb-lvJoin-lvMeet = lvCombine-absorb PartialLatticeType._⊔?_ PartialLatticeType._⊓?_ PartialLatticeType.absorb-⊔-⊓
+
+absorb-lvMeet-lvJoin : ∀ {a} (L : List (PartialLatticeType a)) → PartialAbsorb (eqL L) (lvMeet L) (lvJoin L)
+absorb-lvMeet-lvJoin = lvCombine-absorb PartialLatticeType._⊓?_ PartialLatticeType._⊔?_ PartialLatticeType.absorb-⊓-⊔
+
 lvJoin-greatest-total : ∀ {a} {L : Layer a} →  (lv₁ lv₂ : LayerValue L) →  LayerGreatest L →  lvJoin (toList L) lv₁ lv₂ ≡ nothing → ⊥
 lvJoin-greatest-total {L = plt ∷⁺ []} (inj₁ v₁) (inj₁ v₂) (MkLayerGreatest {{hasGreatest = hasGreatest}}) v₁⊔v₂≡nothing
     with IsPartialLattice.HasGreatestElement.not-partial (PartialLatticeType.isPartialLattice plt) hasGreatest v₁ v₂
@@ -694,9 +770,6 @@ pathJoin'-related' {Ls = Ls} p₁ p₂ p₃ p₂⊔p₃ p₂⊔?p₃=justp₂⊔
         | eqPath'-pathJoin'-cong {Ls = Ls} (eqPath'-refl Ls p₁) p₂⊔p₃≈p₃⊔p₂
 ...     | nothing | nothing | nothing | ≈-nothing | refl | ≈-nothing = refl
 
-
--- fact: pathJoin' Ls p₃ p₂ ≡ just p₃⊔p₂
-
 pathJoin'-assoc : ∀ {a} {Ls : Layers a} → PartialAssoc (eqPath' Ls) (pathJoin' Ls)
 pathJoin'-assoc {Ls = single l} lv₁ lv₂ lv₃ = lvJoin-assoc (toList l) lv₁ lv₂ lv₃
 pathJoin'-assoc {Ls = add-via-least l {{least}} ls} (inj₁ lv₁) (inj₁ lv₂) (inj₁ lv₃)
@@ -777,6 +850,15 @@ pathJoin'-assoc {Ls = add-via-greatest l ls {{greatest = greatest}}} (inj₂ p
 ...   | nothing | _ | _ = ⊥-elim (pathJoin'-greatest-total {Ls = ls} p₁ p₂ greatest p₁⊔?p₂=?)
 ...   | _ | nothing | _ = ⊥-elim (pathJoin'-greatest-total {Ls = ls} p₂ p₃ greatest p₂⊔?p₃=?)
 
+pathJoin'-idemp : ∀ {a} {Ls : Layers a} → PartialIdemp (eqPath' Ls) (pathJoin' Ls)
+pathJoin'-idemp {Ls = single l} lv = lvJoin-idemp (toList l) lv
+pathJoin'-idemp {Ls = add-via-least l ls} (inj₁ lv) = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (lvJoin-idemp (toList l) lv)
+pathJoin'-idemp {Ls = add-via-least l@(plt ∷⁺ []) {{MkLayerLeast {{hasLeast = hasLeast}}}} ls} (inj₂ p)
+    with pathJoin' ls p p | pathJoin'-idemp {Ls = ls} p
+...   | just p⊔p | ≈-just p⊔p≈p = ≈-just p⊔p≈p
+pathJoin'-idemp {Ls = add-via-greatest l ls} (inj₁ lv) = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (lvJoin-idemp (toList l) lv)
+pathJoin'-idemp {Ls = add-via-greatest l ls} (inj₂ p) = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (pathJoin'-idemp {Ls = ls} p)
+
 pathMeet'-comm : ∀ {a} {Ls : Layers a} → PartialComm (eqPath' Ls) (pathMeet' Ls)
 pathMeet'-comm {Ls = single l} lv₁ lv₂ = lvMeet-comm (toList l) lv₁ lv₂
 pathMeet'-comm {Ls = add-via-least l ls} (inj₁ lv₁) (inj₁ lv₂) = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (lvMeet-comm (toList l) lv₁ lv₂)
@@ -800,15 +882,317 @@ pathMeet'-comm {Ls = add-via-greatest l ls {{greatest}}} (inj₂ p₁) (inj₂ p
 pathMeet'-comm {Ls = add-via-greatest l ls} (inj₁ lv₁) (inj₂ p₂) = ≈-just (eqPath'-refl ls p₂)
 pathMeet'-comm {Ls = add-via-greatest l ls} (inj₂ p₁) (inj₁ lv₂) = ≈-just (eqPath'-refl ls p₁)
 
+greatestPath-pathMeet'-identˡ : ∀ {a} (Ls : Layers a) (greatest : LayerGreatest (head Ls))
+                                   (p : Path' Ls) →
+                                   let pᵍ = greatestPath Ls greatest
+                                   in lift-≈ (eqPath' Ls) (pathMeet' Ls pᵍ p) (just p)
+greatestPath-pathMeet'-identˡ (single (plt ∷⁺ []) ) (MkLayerGreatest {{hasGreatest = hasGreatest}}) (inj₁ v)
+    = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (PartialLatticeType.greatest-⊓-identˡ plt hasGreatest v)
+greatestPath-pathMeet'-identˡ (add-via-least (plt ∷⁺ []) ls) (MkLayerGreatest {{hasGreatest = hasGreatest}}) (inj₁ (inj₁ v))
+    = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _
+        (lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (PartialLatticeType.greatest-⊓-identˡ plt hasGreatest v))
+greatestPath-pathMeet'-identˡ (add-via-least l ls) (MkLayerGreatest {{hasGreatest = hasGreatest}}) (inj₂ p) = ≈-just (eqPath'-refl ls p)
+greatestPath-pathMeet'-identˡ {a = a} (add-via-greatest (plt ∷⁺ []) ls) (MkLayerGreatest {{hasGreatest = hasGreatest}}) (inj₁ (inj₁ v))
+    with PartialLatticeType._⊓?_ plt (PartialLatticeType.HasGreatestElement.x {a = a} {plt} hasGreatest) v | PartialLatticeType.greatest-⊓-identˡ plt hasGreatest v
+...   | just vᵍ⊔v | ≈-just vᵍ⊔v≈v = ≈-just vᵍ⊔v≈v
+greatestPath-pathMeet'-identˡ (add-via-greatest l ls) (MkLayerGreatest {{hasGreatest = hasGreatest}}) (inj₂ p) = ≈-just (eqPath'-refl ls p)
+
+greatestPath-pathMeet'-identʳ : ∀ {a} (Ls : Layers a) (greatest : LayerGreatest (head Ls))
+                                   (p : Path' Ls) →
+                                   let pᵍ = greatestPath Ls greatest
+                                   in lift-≈ (eqPath' Ls) (pathMeet' Ls p pᵍ) (just p)
+greatestPath-pathMeet'-identʳ Ls greatest p
+    = IsEquivalence.≈-trans (lift-≈-Equivalence {{eqPath'-Equivalence {Ls = Ls}}})
+        (pathMeet'-comm {Ls = Ls} p (greatestPath Ls greatest))
+        (greatestPath-pathMeet'-identˡ Ls greatest p)
+
+pathMeet'-assoc : ∀ {a} {Ls : Layers a} → PartialAssoc (eqPath' Ls) (pathMeet' Ls)
+pathMeet'-assoc {Ls = single l} lv₁ lv₂ lv₃ = lvMeet-assoc (toList l) lv₁ lv₂ lv₃
+pathMeet'-assoc {Ls = add-via-least l {{least}} ls} (inj₁ lv₁) (inj₁ lv₂) (inj₁ lv₃)
+    rewrite pathMeet'-homo-least₁ l ls least (((` lv₁) ∨ (` lv₂)) ∨ (` lv₃))
+    rewrite pathMeet'-homo-least₁ l ls least ((` lv₁) ∨ ((` lv₂) ∨ (` lv₃)))
+    = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (lvMeet-assoc (toList l) lv₁ lv₂ lv₃)
+pathMeet'-assoc {Ls = add-via-least l@(plt ∷⁺ []) {{MkLayerLeast {{hasLeast = hasLeast}}}} ls} (inj₂ p₁) (inj₁ (inj₁ v₂)) (inj₁ (inj₁ v₃))
+    with PartialLatticeType._⊓?_ plt v₂ v₃ | IsPartialLattice.HasLeastElement.not-partial (PartialLatticeType.isPartialLattice plt) hasLeast v₂ v₃
+...   | just v₂⊓l₃ | (_ , refl) = ≈-just (eqPath'-refl ls p₁)
+pathMeet'-assoc {Ls = add-via-least l {{least}} ls} (inj₁ lv₁) (inj₂ p₂) (inj₁ lv₃)
+    = ≈-just (eqPath'-refl ls p₂)
+pathMeet'-assoc {Ls = add-via-least l {{least}} ls} (inj₂ p₁) (inj₂ p₂) (inj₁ lv₃)
+    with pathMeet' ls p₁ p₂
+...   | just p₁⊓p₂ = ≈-just (eqPath'-refl ls p₁⊓p₂)
+...   | nothing = ≈-nothing
+pathMeet'-assoc {Ls = add-via-least l@(plt ∷⁺ []) {{MkLayerLeast {{hasLeast = hasLeast}}}} ls} (inj₁ (inj₁ v₁)) (inj₁ (inj₁ v₂)) (inj₂ p₃)
+    with PartialLatticeType._⊓?_ plt v₁ v₂ | IsPartialLattice.HasLeastElement.not-partial (PartialLatticeType.isPartialLattice plt) hasLeast v₁ v₂
+...   | just _ | (_ , refl) = ≈-just (eqPath'-refl ls p₃)
+pathMeet'-assoc {Ls = add-via-least l {{least}} ls} (inj₂ p₁) (inj₁ lv₂) (inj₂ p₃)
+    with pathMeet' ls p₁ p₃
+...   | just p₁⊓p₃ = ≈-just (eqPath'-refl ls p₁⊓p₃)
+...   | nothing = ≈-nothing
+pathMeet'-assoc {Ls = add-via-least l {{least}} ls} (inj₁ lv₁) (inj₂ p₂) (inj₂ p₃)
+    with pathMeet' ls p₂ p₃
+...   | just p₂⊓p₃ = ≈-just (eqPath'-refl ls p₂⊓p₃)
+...   | nothing = ≈-nothing
+pathMeet'-assoc {Ls = add-via-least l ls} (inj₂ p₁) (inj₂ p₂) (inj₂ p₃)
+    with pathMeet' ls p₁ p₂ in p₁⊓?p₂=? | pathMeet' ls p₂ p₃ in p₂⊓?p₃=? | pathMeet'-assoc {Ls = ls} p₁ p₂ p₃
+...   | just p₁⊓p₂ | just p₂⊓p₃ | p₁⊓p₂p₃≈p₁p₂⊓p₃ = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ p₁⊓p₂p₃≈p₁p₂⊓p₃
+...   | nothing | nothing | _ = ≈-nothing
+...   | nothing | just p₂⊓p₃ | p₁⊓p₂p₃≈p₁p₂⊓p₃ with nothing ← pathMeet' ls p₁ p₂⊓p₃ = ≈-nothing
+...   | just p₁⊓p₂ | nothing | p₁⊓p₂p₃≈p₁p₂⊓p₃ with nothing ← pathMeet' ls p₁⊓p₂ p₃ = ≈-nothing
+-- begin dumb: due to annoying nested with-abstractions, we have several written-out cases here
+-- for the same inj₁/inj₁/inj₁ combination.
+pathMeet'-assoc {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁) (inj₁ lv₂) (inj₁ lv₃)
+    with lvMeet (toList l) lv₁ lv₂ | lvMeet (toList l) lv₂ lv₃ | lvMeet-assoc (toList l) lv₁ lv₂ lv₃
+...   | just lv₁⊓lv₂ | just lv₂⊓lv₃ | p₁⊓?p₂p₃≈p₁p₂⊓?p₃
+        with lvMeet (toList l) lv₁⊓lv₂ lv₃ | lvMeet (toList l) lv₁ lv₂⊓lv₃ | p₁⊓?p₂p₃≈p₁p₂⊓?p₃
+...       | just _ | just _ | ≈-just p₁⊓p₂p₃≈p₁p₂⊓p₃  = ≈-just p₁⊓p₂p₃≈p₁p₂⊓p₃
+...       | nothing | nothing | ≈-nothing = ≈-just (eqPath'-refl ls (greatestPath ls greatest))
+pathMeet'-assoc {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁) (inj₁ lv₂) (inj₁ lv₃)
+      | nothing | nothing | _ = ≈-just (eqPath'-refl ls (greatestPath ls greatest))
+pathMeet'-assoc {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁) (inj₁ lv₂) (inj₁ lv₃)
+      | just lv₁⊓lv₂ | nothing | p₁⊓?p₂p₃≈p₁p₂⊓?p₃
+        with nothing <- lvMeet (toList l) lv₁⊓lv₂ lv₃ = ≈-just (eqPath'-refl ls (greatestPath ls greatest))
+pathMeet'-assoc {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁) (inj₁ lv₂) (inj₁ lv₃)
+      | nothing | just lv₂⊓lv₃ | p₁⊓?p₂p₃≈p₁p₂⊓?p₃
+        with nothing <- lvMeet (toList l) lv₁ lv₂⊓lv₃ = ≈-just (eqPath'-refl ls (greatestPath ls greatest))
+-- end dumb
+pathMeet'-assoc {Ls = add-via-greatest l ls {{greatest}}} (inj₂ p₁) (inj₁ lv₂) (inj₁ lv₃)
+    with lvMeet (toList l) lv₂ lv₃
+...   | just _ = ≈-just (eqPath'-refl ls p₁)
+...   | nothing = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (IsEquivalence.≈-sym (lift-≈-Equivalence {{eqPath'-Equivalence {Ls = ls}}}) (greatestPath-pathMeet'-identʳ ls greatest p₁))
+pathMeet'-assoc {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁) (inj₂ p₂) (inj₁ lv₃)
+    = ≈-just (eqPath'-refl ls p₂)
+pathMeet'-assoc {Ls = add-via-greatest l ls {{greatest}}} (inj₂ p₁) (inj₂ p₂) (inj₁ lv₃)
+    with pathMeet' ls p₁ p₂
+...   | just p₁⊓p₂ = ≈-just (eqPath'-refl ls p₁⊓p₂)
+...   | nothing = ≈-nothing
+pathMeet'-assoc {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁) (inj₁ lv₂) (inj₂ p₃)
+    with lvMeet (toList l) lv₁ lv₂
+...   | just _ = ≈-just (eqPath'-refl ls p₃)
+...   | nothing = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (greatestPath-pathMeet'-identˡ ls greatest p₃)
+pathMeet'-assoc {Ls = add-via-greatest l ls {{greatest}}} (inj₂ p₁) (inj₁ lv₂) (inj₂ p₃)
+    with pathMeet' ls p₁ p₃
+...   | just p₁⊓p₃ = ≈-just (eqPath'-refl ls p₁⊓p₃)
+...   | nothing = ≈-nothing
+pathMeet'-assoc {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁) (inj₂ p₂) (inj₂ p₃)
+    with pathMeet' ls p₂ p₃
+...   | just p₂⊓p₃ = ≈-just (eqPath'-refl ls p₂⊓p₃)
+...   | nothing = ≈-nothing
+pathMeet'-assoc {Ls = add-via-greatest l ls {{greatest}}} (inj₂ p₁) (inj₂ p₂) (inj₂ p₃)
+    with pathMeet' ls p₁ p₂ in p₁⊓?p₂=? | pathMeet' ls p₂ p₃ in p₂⊓?p₃=? | pathMeet'-assoc {Ls = ls} p₁ p₂ p₃
+...   | just p₁⊓p₂ | just p₂⊓p₃ | p₁⊓p₂p₃≈p₁p₂⊓p₃ = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ p₁⊓p₂p₃≈p₁p₂⊓p₃
+...   | nothing | nothing | _ = ≈-nothing
+...   | nothing | just p₂⊓p₃ | p₁⊓p₂p₃≈p₁p₂⊓p₃ with nothing ← pathMeet' ls p₁ p₂⊓p₃ = ≈-nothing
+...   | just p₁⊓p₂ | nothing | p₁⊓p₂p₃≈p₁p₂⊓p₃ with nothing ← pathMeet' ls p₁⊓p₂ p₃ = ≈-nothing
+
+pathMeet'-idemp : ∀ {a} {Ls : Layers a} → PartialIdemp (eqPath' Ls) (pathMeet' Ls)
+pathMeet'-idemp {Ls = single l} lv = lvMeet-idemp (toList l) lv
+pathMeet'-idemp {Ls = add-via-least l ls} (inj₁ lv) = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (lvMeet-idemp (toList l) lv)
+pathMeet'-idemp {Ls = add-via-least l ls} (inj₂ p) = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (pathMeet'-idemp {Ls = ls} p)
+pathMeet'-idemp {Ls = add-via-greatest l ls} (inj₁ lv)
+    with lvMeet (toList l) lv lv | lvMeet-idemp (toList l) lv
+...   | just lv⊔lv | ≈-just lv⊔lv≈lv = ≈-just lv⊔lv≈lv
+pathMeet'-idemp {Ls = add-via-greatest l ls} (inj₂ p) = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (pathMeet'-idemp {Ls = ls} p)
+
+absorb-pathJoin'-pathMeet' : ∀ {a} {Ls : Layers a} → PartialAbsorb (eqPath' Ls) (pathJoin' Ls) (pathMeet' Ls)
+absorb-pathJoin'-pathMeet' {Ls = single l} lv₁ lv₂ = absorb-lvJoin-lvMeet (toList l) lv₁ lv₂
+absorb-pathJoin'-pathMeet' {Ls = Ls@(add-via-least l ls)} (inj₁ lv₁) (inj₁ lv₂)
+    = PartialAbsorb-map inj₁ _ _ (λ _ _ x → x) (lvJoin (toList l)) (lvMeet (toList l))
+                                 (pathJoin' Ls) (pathMeet' Ls)
+                                 (λ _ _ → refl) (λ _ _ → refl)
+                                 (absorb-lvJoin-lvMeet (toList l)) lv₁ lv₂
+absorb-pathJoin'-pathMeet' {Ls = add-via-least l {{least}} ls} (inj₂ p₁) (inj₁ lv₂)
+    = pathJoin'-idemp {Ls = add-via-least l {{least}} ls} (inj₂ p₁)
+absorb-pathJoin'-pathMeet' {Ls = add-via-least l ls} (inj₁ lv₁) (inj₂ p₂)
+    = ≈-just (eqLv-refl l lv₁)
+absorb-pathJoin'-pathMeet' {Ls = add-via-least l@(plt ∷⁺ []) {{MkLayerLeast {{hasLeast = hasLeast}}}} ls} (inj₂ p₁) (inj₂ p₂)
+    with pathMeet' ls p₁ p₂ | absorb-pathJoin'-pathMeet' {Ls = ls} p₁ p₂
+...   | nothing | _ = mkTrivial
+...   | just p₁⊓p₂ | p₁⊔p₁p₂≈?p₁
+        with pathJoin' ls p₁ p₁⊓p₂ | p₁⊔p₁p₂≈?p₁
+...       | just _ | ≈-just p₁⊔p₁p₂≈p₁ = ≈-just p₁⊔p₁p₂≈p₁
+absorb-pathJoin'-pathMeet' {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁) (inj₁ lv₂)
+    with lvMeet (toList l) lv₁ lv₂ | absorb-lvJoin-lvMeet (toList l) lv₁ lv₂
+...   | nothing | _ = ≈-just (eqLv-refl l lv₁)
+...   | just lv₁⊓lv₂ | lv₁⊔lv₁lv₂≈?lv₁
+        with lvJoin (toList l) lv₁ lv₁⊓lv₂ | lv₁⊔lv₁lv₂≈?lv₁
+...       | just _ | ≈-just lv₁⊔lv₁lv₂≈lv₁ = ≈-just lv₁⊔lv₁lv₂≈lv₁
+absorb-pathJoin'-pathMeet' {Ls = add-via-greatest l ls {{greatest}} } (inj₂ p₁) (inj₁ lv₂)
+    = pathJoin'-idemp {Ls = add-via-greatest l ls {{greatest}}} (inj₂ p₁)
+absorb-pathJoin'-pathMeet' {Ls = add-via-greatest l ls} (inj₁ lv₁) (inj₂ p₂)
+    = ≈-just (eqLv-refl l lv₁)
+absorb-pathJoin'-pathMeet' {Ls = Ls@(add-via-greatest l ls)} (inj₂ p₁) (inj₂ p₂)
+    = PartialAbsorb-map inj₂ _ _ (λ _ _ x → x) (pathJoin' ls) (pathMeet' ls)
+                                 (pathJoin' Ls) (pathMeet' Ls)
+                                 (λ _ _ → refl) (λ _ _ → refl)
+                                 (absorb-pathJoin'-pathMeet' {Ls = ls}) p₁ p₂
+
+absorb-pathMeet'-pathJoin' : ∀ {a} {Ls : Layers a} → PartialAbsorb (eqPath' Ls) (pathMeet' Ls) (pathJoin' Ls)
+absorb-pathMeet'-pathJoin' {Ls = single l} lv₁ lv₂ = absorb-lvMeet-lvJoin (toList l) lv₁ lv₂
+absorb-pathMeet'-pathJoin' {Ls = Ls@(add-via-least l ls)} (inj₁ lv₁) (inj₁ lv₂)
+    = PartialAbsorb-map inj₁ _ _ (λ _ _ x → x) (lvMeet (toList l)) (lvJoin (toList l))
+                                 (pathMeet' Ls) (pathJoin' Ls)
+                                 (λ _ _ → refl) (λ _ _ → refl)
+                                 (absorb-lvMeet-lvJoin (toList l)) lv₁ lv₂
+absorb-pathMeet'-pathJoin' {Ls = add-via-least l ls} (inj₂ p₁) (inj₁ lv₂)
+    = ≈-just (eqPath'-refl ls p₁)
+absorb-pathMeet'-pathJoin' {Ls = add-via-least l {{least}} ls} (inj₁ lv₁) (inj₂ p₂)
+    = pathMeet'-idemp {Ls = add-via-least l {{least}} ls} (inj₁ lv₁)
+absorb-pathMeet'-pathJoin' {Ls = add-via-least l@(plt ∷⁺ []) {{MkLayerLeast {{hasLeast = hasLeast}}}} ls} (inj₂ p₁) (inj₂ p₂)
+    with pathJoin' ls p₁ p₂ | absorb-pathMeet'-pathJoin' {Ls = ls} p₁ p₂
+...   | nothing | _ = ≈-just (eqPath'-refl ls p₁)
+...   | just p₁⊓p₂ | p₁⊔p₁p₂≈?p₁
+        with pathMeet' ls p₁ p₁⊓p₂ | p₁⊔p₁p₂≈?p₁
+...       | just _ | ≈-just p₁⊔p₁p₂≈p₁ = ≈-just p₁⊔p₁p₂≈p₁
+absorb-pathMeet'-pathJoin' {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁) (inj₁ lv₂)
+    with lvJoin (toList l) lv₁ lv₂ | absorb-lvMeet-lvJoin (toList l) lv₁ lv₂
+...   | nothing | _ = mkTrivial
+...   | just lv₁⊓lv₂ | lv₁⊔lv₁lv₂≈?lv₁
+        with lvMeet (toList l) lv₁ lv₁⊓lv₂ | lv₁⊔lv₁lv₂≈?lv₁
+...       | just _ | ≈-just lv₁⊔lv₁lv₂≈lv₁ = ≈-just lv₁⊔lv₁lv₂≈lv₁
+absorb-pathMeet'-pathJoin' {Ls = add-via-greatest l ls} (inj₂ p₁) (inj₁ lv₂)
+    = ≈-just (eqPath'-refl ls p₁)
+absorb-pathMeet'-pathJoin' {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁) (inj₂ p₂)
+    = pathMeet'-idemp {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁)
+absorb-pathMeet'-pathJoin' {Ls = Ls@(add-via-greatest l ls)} (inj₂ p₁) (inj₂ p₂)
+    = PartialAbsorb-map inj₂ _ _ (λ _ _ x → x) (pathMeet' ls) (pathJoin' ls)
+                                 (pathMeet' Ls) (pathJoin' Ls)
+                                 (λ _ _ → refl) (λ _ _ → refl)
+                                 (absorb-pathMeet'-pathJoin' {Ls = ls}) p₁ p₂
+
+
 record _≈_ {a} {Ls : Layers a} (p₁ p₂ : Path Ls) : Set a where
+    constructor mk-≈
     field pathEq : eqPath' Ls (Path.path p₁) (Path.path p₂)
 
+instance
+    ≈-Equivalence : ∀ {a} {Ls : Layers a} → IsEquivalence (Path Ls) (_≈_ {Ls = Ls})
+    ≈-Equivalence {Ls = Ls} =
+        record
+            { ≈-refl = λ {(MkPath p)} → mk-≈ (eqPath'-refl Ls p)
+            ; ≈-sym = λ (mk-≈ p≈p') →  mk-≈ (eqPath'-sym Ls p≈p')
+            ; ≈-trans = λ (mk-≈ p₁≈p₂) (mk-≈ p₂≈p₃) → mk-≈ (eqPath'-trans Ls p₁≈p₂ p₂≈p₃)
+            }
+
 _⊔̇_ : ∀ {a} {Ls : Layers a} (p₁ p₂ : Path Ls) → Maybe (Path Ls)
 _⊔̇_ {a} {ls} p₁ p₂ = Maybe.map MkPath (pathJoin' ls (Path.path p₁) (Path.path p₂))
 
+_⊔̇_-subHomo : ∀ {a} (Ls : Layers a) (e : Expr (Path' Ls)) → eval (_⊔̇_ {Ls = Ls}) (map MkPath e) ≡ Maybe.map MkPath (eval (pathJoin' Ls) e)
+_⊔̇_-subHomo Ls e = eval-subHomo MkPath (pathJoin' Ls) _⊔̇_ e (λ a₁ a₂ → refl)
+
+_⊔̇_-comm : ∀ {a} {Ls : Layers a} → PartialComm (_≈_ {Ls = Ls}) (_⊔̇_ {Ls = Ls})
+_⊔̇_-comm {Ls = Ls} (MkPath p₁) (MkPath p₂)
+    = lift-≈-map MkPath _ (_≈_ {Ls = Ls}) (λ _ _ → mk-≈) _ _ (pathJoin'-comm {Ls = Ls} p₁ p₂)
+
+_⊔̇_-assoc : ∀ {a} {Ls : Layers a} → PartialAssoc (_≈_ {Ls = Ls}) (_⊔̇_ {Ls = Ls})
+_⊔̇_-assoc {Ls = Ls} (MkPath p₁) (MkPath p₂) (MkPath p₃)
+    rewrite _⊔̇_-subHomo Ls (((` p₁) ∨ (` p₂)) ∨ (` p₃))
+    rewrite _⊔̇_-subHomo Ls ((` p₁) ∨ ((` p₂) ∨ (` p₃)))
+    = lift-≈-map MkPath _ (_≈_ {Ls = Ls}) (λ _ _ → mk-≈) _ _ (pathJoin'-assoc {Ls = Ls} p₁ p₂ p₃)
+
+_⊔̇_-idemp : ∀ {a} {Ls : Layers a} → PartialIdemp (_≈_ {Ls = Ls}) (_⊔̇_ {Ls = Ls})
+_⊔̇_-idemp {Ls = Ls} (MkPath p)
+    = lift-≈-map MkPath _ (_≈_ {Ls = Ls}) (λ _ _ → mk-≈) _ _ (pathJoin'-idemp {Ls = Ls} p)
+
+≈-⊔̇-cong : ∀ {a} {Ls : Layers a} → PartialCong (_≈_ {Ls = Ls}) (_⊔̇_ {Ls = Ls})
+≈-⊔̇-cong {Ls = Ls} (mk-≈ p₁≈p₂) (mk-≈ p₃≈p₄) =
+    lift-≈-map MkPath _ (_≈_ {Ls = Ls}) (λ _ _ → mk-≈) _ _ (eqPath'-pathJoin'-cong {Ls = Ls} p₁≈p₂ p₃≈p₄)
+
 _⊓̇_ : ∀ {a} {Ls : Layers a} (p₁ p₂ : Path Ls) → Maybe (Path Ls)
 _⊓̇_ {a} {ls} p₁ p₂ = Maybe.map MkPath (pathMeet' ls (Path.path p₁) (Path.path p₂))
 
+_⊓̇_-subHomo : ∀ {a} (Ls : Layers a) (e : Expr (Path' Ls)) → eval (_⊓̇_ {Ls = Ls}) (map MkPath e) ≡ Maybe.map MkPath (eval (pathMeet' Ls) e)
+_⊓̇_-subHomo Ls e = eval-subHomo MkPath (pathMeet' Ls) _⊓̇_ e (λ a₁ a₂ → refl)
+
+_⊓̇_-comm : ∀ {a} {Ls : Layers a} → PartialComm (_≈_ {Ls = Ls}) (_⊓̇_ {Ls = Ls})
+_⊓̇_-comm {Ls = Ls} (MkPath p₁) (MkPath p₂)
+    = lift-≈-map MkPath _ (_≈_ {Ls = Ls}) (λ _ _ → mk-≈) _ _ (pathMeet'-comm {Ls = Ls} p₁ p₂)
+
+_⊓̇_-assoc : ∀ {a} {Ls : Layers a} → PartialAssoc (_≈_ {Ls = Ls}) (_⊓̇_ {Ls = Ls})
+_⊓̇_-assoc {Ls = Ls} (MkPath p₁) (MkPath p₂) (MkPath p₃)
+    rewrite _⊓̇_-subHomo Ls (((` p₁) ∨ (` p₂)) ∨ (` p₃))
+    rewrite _⊓̇_-subHomo Ls ((` p₁) ∨ ((` p₂) ∨ (` p₃)))
+    = lift-≈-map MkPath _ (_≈_ {Ls = Ls}) (λ _ _ → mk-≈) _ _ (pathMeet'-assoc {Ls = Ls} p₁ p₂ p₃)
+
+_⊓̇_-idemp : ∀ {a} {Ls : Layers a} → PartialIdemp (_≈_ {Ls = Ls}) (_⊓̇_ {Ls = Ls})
+_⊓̇_-idemp {Ls = Ls} (MkPath p)
+    = lift-≈-map MkPath _ (_≈_ {Ls = Ls}) (λ _ _ → mk-≈) _ _ (pathMeet'-idemp {Ls = Ls} p)
+
+≈-⊓̇-cong : ∀ {a} {Ls : Layers a} → PartialCong (_≈_ {Ls = Ls}) (_⊓̇_ {Ls = Ls})
+≈-⊓̇-cong {Ls = Ls} (mk-≈ p₁≈p₂) (mk-≈ p₃≈p₄) =
+    lift-≈-map MkPath _ (_≈_ {Ls = Ls}) (λ _ _ → mk-≈) _ _ (eqPath'-pathMeet'-cong {Ls = Ls} p₁≈p₂ p₃≈p₄)
+
+instance
+    Path-IsPartialJoinSemilattice : ∀ {a} {Ls : Layers a} → IsPartialSemilattice (_≈_ {Ls = Ls}) (_⊔̇_ {Ls = Ls})
+    Path-IsPartialJoinSemilattice {Ls = Ls} =
+        record
+            { ⊔-assoc = _⊔̇_-assoc {Ls = Ls}
+            ; ⊔-comm = _⊔̇_-comm {Ls = Ls}
+            ; ⊔-idemp = _⊔̇_-idemp {Ls = Ls}
+            ; ≈-⊔-cong = ≈-⊔̇-cong {Ls = Ls}
+            }
+
+    Path-IsPartialMeetSemilattice : ∀ {a} {Ls : Layers a} → IsPartialSemilattice (_≈_ {Ls = Ls}) (_⊓̇_ {Ls = Ls})
+    Path-IsPartialMeetSemilattice {Ls = Ls} =
+        record
+            { ⊔-assoc = _⊓̇_-assoc {Ls = Ls}
+            ; ⊔-comm = _⊓̇_-comm {Ls = Ls}
+            ; ⊔-idemp = _⊓̇_-idemp {Ls = Ls}
+            ; ≈-⊔-cong = ≈-⊓̇-cong {Ls = Ls}
+            }
+
+⊔̇-⊓̇-absorb : ∀ {a} {Ls : Layers a} → PartialAbsorb (_≈_ {Ls = Ls}) (_⊔̇_ {Ls = Ls}) (_⊓̇_ {Ls = Ls})
+⊔̇-⊓̇-absorb {Ls = Ls} (MkPath p₁) (MkPath p₂)
+    = PartialAbsorb-map MkPath _ _ (λ _ _ → mk-≈) (pathJoin' Ls) (pathMeet' Ls)
+                                   (_⊔̇_ {Ls = Ls}) (_⊓̇_ {Ls = Ls})
+                                   (λ _ _ → refl) (λ _ _ → refl)
+                                   (absorb-pathJoin'-pathMeet' {Ls = Ls}) p₁ p₂
+
+⊓̇-⊔̇-absorb : ∀ {a} {Ls : Layers a} → PartialAbsorb (_≈_ {Ls = Ls}) (_⊓̇_ {Ls = Ls}) (_⊔̇_ {Ls = Ls})
+⊓̇-⊔̇-absorb {Ls = Ls} (MkPath p₁) (MkPath p₂)
+    = PartialAbsorb-map MkPath _ _ (λ _ _ → mk-≈) (pathMeet' Ls) (pathJoin' Ls)
+                                   (_⊓̇_ {Ls = Ls}) (_⊔̇_ {Ls = Ls})
+                                   (λ _ _ → refl) (λ _ _ → refl)
+                                   (absorb-pathMeet'-pathJoin' {Ls = Ls}) p₁ p₂
+
+instance
+    Path-IsPartialLattice : ∀ {a} {Ls : Layers a} → IsPartialLattice (_≈_ {Ls = Ls}) (_⊔̇_ {Ls = Ls}) (_⊓̇_ {Ls = Ls})
+    Path-IsPartialLattice {Ls = Ls} =
+        record
+            { absorb-⊔-⊓ = ⊔̇-⊓̇-absorb {Ls = Ls}
+            ; absorb-⊓-⊔ = ⊓̇-⊔̇-absorb {Ls = Ls}
+            }
+
+instance
+    -- IsLattice-IsPartialLattice : ∀ {a} {A : Set a}
+    --     {_≈_ : A → A → Set a} {_⊔_ : A → A → A} {_⊓_ : A → A → A}
+    --     {{lA : IsLattice A _≈_ _⊔_ _⊓_}} → IsPartialLattice _≈_ _⊔_ _⊓_
+    -- IsLattice-IsPartialLattice = {!!}
+
+    Lattice-PartialLattice : ∀ {a} {A : Set a}
+        {{lA : Lattice A }} →  PartialLattice A
+    Lattice-PartialLattice = {!!}
+
+    Lattice-Least : ∀ {a} {A : Set a}
+        {{lA : Lattice A }} → PartialLattice.HasLeastElement (Lattice-PartialLattice {{lA = lA}})
+    Lattice-Least = {!!}
+
+open import Lattice.Unit
+
+ThreeElements : Set
+ThreeElements = Path (add-via-least ((mkPartialLatticeType ⊤) ∷⁺ []) (add-via-least ((mkPartialLatticeType ⊤) ∷⁺ []) (single ((mkPartialLatticeType ⊤) ∷⁺ []))))
+
+e₁ : ThreeElements
+e₁ = MkPath (inj₁ (inj₁ tt))
+
+e₂ : ThreeElements
+e₂ = MkPath (inj₂ (inj₁ (inj₁ tt)))
+
+e₃ : ThreeElements
+e₃ = MkPath (inj₂ (inj₂ (inj₁ tt)))
+
+ex1 : e₁ ⊔̇ e₂ ≡ just e₁
+ex1 = refl
+
 -- data ListValue {a : Level} : List (PartialLatticeType a) → Set (lsuc a) where
 --     here : ∀ {plt : PartialLatticeType a} {pltl : List (PartialLatticeType a)}
 --              (v : PartialLatticeType.EltType plt) → ListValue (plt ∷ pltl)