Skip to content

Commit 54a2b1f

Browse files
committed
Fix whitespace
1 parent a181af8 commit 54a2b1f

File tree

2 files changed

+2
-3
lines changed

2 files changed

+2
-3
lines changed

Cubical/HITs/Wedge/Properties.agda

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -618,7 +618,7 @@ module _ (X∙ @ (X , x₀) : Pointed ℓ) (Y∙ @ (Y , y₀) : Pointed ℓ') wh
618618
{-
619619
The proof proceeds by applying the pasting lemma twice:
620620
1 ----> Y
621-
↓ ↓
621+
↓ ↓
622622
X --> X ⋁ Y --> X
623623
↓ mid ↓ bot ↓
624624
1 ----> Y ----> 1
@@ -646,6 +646,6 @@ module _ (X∙ @ (X , x₀) : Pointed ℓ) (Y∙ @ (Y , y₀) : Pointed ℓ') wh
646646
where
647647
open PushoutPasteDown (rotatePushoutSquare (_ , midPushout))
648648
fX (terminal X) (terminal Y) refl
649-
649+
650650
Pushout⋁≃Unit : Pushout fX fY ≃ Unit
651651
Pushout⋁≃Unit = _ , botPushout

Cubical/Homotopy/Loopspace.agda

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -538,4 +538,3 @@ module _ {ℓ} {B C : Type ℓ} (b₀ : B) (π : B → C) where
538538
-- splitting and splitting∙ agrees
539539
splitting-typ : cong typ splitting∙ ≡ splitting
540540
splitting-typ = congFunct typ presplit twisted∙
541-

0 commit comments

Comments
 (0)