diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda
index 88f53ac..68a7da7 100644
--- a/Lattice/Builder.agda
+++ b/Lattice/Builder.agda
@@ -465,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.