Delete debugging code

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

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 _≈_ _⊔?_
@@ -304,6 +304,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 +319,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 +465,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.
 
@@ -514,6 +540,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)) →
@@ -694,9 +723,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 +803,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 +835,197 @@ 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)
+
 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}
+            }
+
 -- 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)