diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda
index b0dba7a..88f53ac 100644
--- a/Lattice/Builder.agda
+++ b/Lattice/Builder.agda
@@ -807,7 +807,7 @@ pathMeet'-comm {Ls = add-via-greatest l ls} (inj₁ lv₁) (inj₂ p₂) = ≈-j
 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) → 
+                                   (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)
@@ -822,7 +822,7 @@ greatestPath-pathMeet'-identˡ {a = a} (add-via-greatest (plt ∷⁺ []) ls) (Mk
 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) → 
+                                   (p : Path' Ls) →
                                    let pᵍ = greatestPath Ls greatest
                                    in lift-≈ (eqPath' Ls) (pathMeet' Ls p pᵍ) (just p)
 greatestPath-pathMeet'-identʳ Ls greatest p