From 13eee932553b3d5af9bb911a548e538955498f27 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Fri, 25 Jul 2025 15:26:41 +0200 Subject: [PATCH] Remove whitespace errors Signed-off-by: Danila Fedorin --- Lattice/Builder.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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