From 54a2b1fa49ef4a26a62ff52f0f3ba9fa412ebe36 Mon Sep 17 00:00:00 2001 From: Trebor-Huang Date: Thu, 19 Sep 2024 21:42:05 +0800 Subject: [PATCH] Fix whitespace --- Cubical/HITs/Wedge/Properties.agda | 4 ++-- Cubical/Homotopy/Loopspace.agda | 1 - 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/Cubical/HITs/Wedge/Properties.agda b/Cubical/HITs/Wedge/Properties.agda index ba496a408..60043a6a8 100644 --- a/Cubical/HITs/Wedge/Properties.agda +++ b/Cubical/HITs/Wedge/Properties.agda @@ -618,7 +618,7 @@ module _ (X∙ @ (X , x₀) : Pointed ℓ) (Y∙ @ (Y , y₀) : Pointed ℓ') wh {- The proof proceeds by applying the pasting lemma twice: 1 ----> Y - ↓ ↓ + ↓ ↓ X --> X ⋁ Y --> X ↓ mid ↓ bot ↓ 1 ----> Y ----> 1 @@ -646,6 +646,6 @@ module _ (X∙ @ (X , x₀) : Pointed ℓ) (Y∙ @ (Y , y₀) : Pointed ℓ') wh where open PushoutPasteDown (rotatePushoutSquare (_ , midPushout)) fX (terminal X) (terminal Y) refl - + Pushout⋁≃Unit : Pushout fX fY ≃ Unit Pushout⋁≃Unit = _ , botPushout diff --git a/Cubical/Homotopy/Loopspace.agda b/Cubical/Homotopy/Loopspace.agda index 9b74e0a59..2f687d7ab 100644 --- a/Cubical/Homotopy/Loopspace.agda +++ b/Cubical/Homotopy/Loopspace.agda @@ -538,4 +538,3 @@ module _ {ℓ} {B C : Type ℓ} (b₀ : B) (π : B → C) where -- splitting and splitting∙ agrees splitting-typ : cong typ splitting∙ ≡ splitting splitting-typ = congFunct typ presplit twisted∙ - \ No newline at end of file