diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda
index 8102dfa..9ad74bb 100644
--- a/Lattice/Builder.agda
+++ b/Lattice/Builder.agda
@@ -334,6 +334,22 @@ instance
         ; ≈-refl = λ {lv} → eqL-refl L lv
         }
 
+eqL-lvCombine-cong : ∀ {a} (f : CombineForPLT a) →
+                     (∀ plt →  PartialCong (PartialLatticeType._≈_ plt) (f plt)) →
+                     ∀ (L : List (PartialLatticeType a)) →
+                     PartialCong (eqL L) (lvCombine f L)
+eqL-lvCombine-cong f f-Cong [] {()}
+eqL-lvCombine-cong f f-Cong (plt ∷ plts) {inj₁ v₁} {inj₁ v₂} {inj₁ v₃} {inj₁ v₄} v₁≈v₂ v₃≈v₄
+    with f plt v₁ v₃ | f plt v₂ v₄ | f-Cong plt v₁≈v₂ v₃≈v₄
+...   | just _ | just _ | ≈-just v₁⊗v₃≈v₂⊗v₄ = ≈-just v₁⊗v₃≈v₂⊗v₄
+...   | nothing | nothing | ≈-nothing = ≈-nothing
+eqL-lvCombine-cong f f-Cong (plt ∷ plts) {inj₂ lv₁} {inj₂ lv₂} {inj₁ v₃} {inj₁ v₄} _ _ = ≈-nothing
+eqL-lvCombine-cong f f-Cong (plt ∷ plts) {inj₁ v₁} {inj₁ v₂} {inj₂ lv₃} {inj₂ lv₄} _ _ = ≈-nothing
+eqL-lvCombine-cong f f-Cong (plt ∷ plts) {inj₂ lv₁} {inj₂ lv₂} {inj₂ lv₃} {inj₂ lv₄} lv₁≈lv₂ lv₃≈lv₄
+    with lvCombine f plts lv₁ lv₃ | lvCombine f plts lv₂ lv₄ | eqL-lvCombine-cong f f-Cong plts {lv₁} {lv₂} {lv₃} {lv₄} lv₁≈lv₂ lv₃≈lv₄
+...   | just _ | just _ | ≈-just lv₁⊗v₃≈v₂⊗v₄ = ≈-just lv₁⊗v₃≈v₂⊗v₄
+...   | nothing | nothing | ≈-nothing = ≈-nothing
+
 eqLv : ∀ {a} (L : Layer a) →  LayerValue L → LayerValue L → Set a
 eqLv L = eqL (toList L)
 
@@ -354,6 +370,18 @@ instance
         ; ≈-refl = λ {lv} → eqLv-refl L lv
         }
 
+eqLv-lvCombine-cong : ∀ {a} (f : CombineForPLT a) →
+                      (∀ plt →  PartialCong (PartialLatticeType._≈_ plt) (f plt)) →
+                      ∀ (L : Layer a) →
+                      PartialCong (eqLv L) (lvCombine f (toList L))
+eqLv-lvCombine-cong f f-Cong L {lv₁} {lv₂} {lv₃} {lv₄} = eqL-lvCombine-cong f f-Cong (toList L) {lv₁} {lv₂} {lv₃} {lv₄}
+
+eqLv-lvJoin-cong : ∀ {a} (L : Layer a) → PartialCong (eqLv L) (lvJoin (toList L))
+eqLv-lvJoin-cong = eqLv-lvCombine-cong PartialLatticeType._⊔?_ PartialLatticeType.≈-⊔-cong
+
+eqLv-lvMeet-cong : ∀ {a} (L : Layer a) → PartialCong (eqLv L) (lvMeet (toList L))
+eqLv-lvMeet-cong = eqLv-lvCombine-cong PartialLatticeType._⊓?_ PartialLatticeType.≈-⊓-cong
+
 eqPath' : ∀ {a} (Ls : Layers a) → Path' Ls → Path' Ls → Set a
 eqPath' (single l) lv₁ lv₂ = eqLv l lv₁ lv₂
 eqPath' (add-via-least l ls) (inj₁ lv₁) (inj₁ lv₂) = eqLv l lv₁ lv₂
@@ -394,6 +422,29 @@ instance
         ; ≈-refl = λ {x} → eqPath'-refl Ls x
         }
 
+eqPath'-pathJoin'-cong : ∀ {a} {Ls : Layers a} {a₁ a₂ a₃ a₄} →  eqPath' Ls a₁ a₂ →  eqPath' Ls a₃ a₄ →  lift-≈ (eqPath' Ls) (pathJoin' Ls a₁ a₃) (pathJoin' Ls a₂ a₄)
+eqPath'-pathJoin'-cong {Ls = single l} {lv₁} {lv₂} {lv₃} {lv₄} lv₁≈lv₂ lv₃≈lv₄ = eqLv-lvJoin-cong l {lv₁} {lv₂} {lv₃} {lv₄} lv₁≈lv₂ lv₃≈lv₄
+eqPath'-pathJoin'-cong {Ls = add-via-least l ls} {inj₁ lv₁} {inj₁ lv₂} {inj₁ lv₃} {inj₁ lv₄} lv₁≈lv₂ lv₃≈lv₄
+    with lvJoin (toList l) lv₁ lv₃ | lvJoin (toList l) lv₂ lv₄ | eqLv-lvJoin-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'-pathJoin'-cong {Ls = add-via-least l ls} {inj₂ p₁} {inj₂ p₂} {inj₁ lv₃} {inj₁ lv₄} p₁≈p₂ lv₃≈lv₄ = ≈-just lv₃≈lv₄
+eqPath'-pathJoin'-cong {Ls = add-via-least l ls} {inj₁ lv₁} {inj₁ lv₂} {inj₂ p₃} {inj₂ p₄} lv₁≈lv₂ p₃≈p₄ = ≈-just lv₁≈lv₂
+eqPath'-pathJoin'-cong {Ls = Ls@(add-via-least l@(plt ∷⁺ []) {{MkLayerLeast {{hasLeast = hasLeast}}}} ls)} {inj₂ p₁} {inj₂ p₂} {inj₂ p₃} {inj₂ p₄} p₁≈p₂ p₃≈p₄
+    with pathJoin' ls p₁ p₃ | pathJoin' ls p₂ p₄ | eqPath'-pathJoin'-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 = ≈-just (eqPath'-refl Ls (inj₁ (inj₁ (PartialLatticeType.HasLeastElement.x {_} {plt} hasLeast))))
+eqPath'-pathJoin'-cong {Ls = add-via-greatest l ls} {inj₁ lv₁} {inj₁ lv₂} {inj₁ lv₃} {inj₁ lv₄} lv₁≈lv₂ lv₃≈lv₄
+    with lvJoin (toList l) lv₁ lv₃ | lvJoin (toList l) lv₂ lv₄ | eqLv-lvJoin-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'-pathJoin'-cong {Ls = add-via-greatest l ls} {inj₂ p₁} {inj₂ p₂} {inj₁ lv₃} {inj₁ lv₄} p₁≈p₂ lv₃≈lv₄ = ≈-just lv₃≈lv₄
+eqPath'-pathJoin'-cong {Ls = add-via-greatest l ls} {inj₁ lv₁} {inj₁ lv₂} {inj₂ p₃} {inj₂ p₄} lv₁≈lv₂ p₃≈p₄ = ≈-just lv₁≈lv₂
+eqPath'-pathJoin'-cong {Ls = add-via-greatest l ls {{greatest}}} {inj₂ p₁} {inj₂ p₂} {inj₂ p₃} {inj₂ p₄} p₁≈p₂ p₃≈p₄
+    with pathJoin' ls p₁ p₃ | pathJoin' ls p₂ p₄ | eqPath'-pathJoin'-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.