diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda
index 62ebae7..d17c730 100644
--- a/Lattice/Builder.agda
+++ b/Lattice/Builder.agda
@@ -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
-        with head ls | greatest | valueAtHead ls
-...       | _ | MkLayerGreatest {{hasGreatest = hasGreatest}} | vah
-          = just (inj₂ (vah (inj₁ (IsPartialSemilattice.HasAbsorbingElement.x hasGreatest))))
+...   | nothing = just (inj₂ (greatestPath ls greatest))
 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₂)