From c9721bacd6d93ef733079c9dde10bf64e338f24f Mon Sep 17 00:00:00 2001 From: Trebor-Huang Date: Sun, 18 Aug 2024 00:08:43 +0800 Subject: [PATCH] tweak --- Cubical/HITs/Join/SuspWedgeEquiv.agda | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Cubical/HITs/Join/SuspWedgeEquiv.agda b/Cubical/HITs/Join/SuspWedgeEquiv.agda index 175103449..05a2092c2 100644 --- a/Cubical/HITs/Join/SuspWedgeEquiv.agda +++ b/Cubical/HITs/Join/SuspWedgeEquiv.agda @@ -121,6 +121,5 @@ module _ {ℓ ℓ'} (X∙ @ (X , x₀) : Pointed ℓ) (Y∙ @ (Y , y₀) : Point H3 = λ _ → refl } ∙ sym (Susp≡PushoutSusp* {ℓ-max ℓ ℓ'}) - join≡Susp : Susp (X∙ ⋀ Y∙) ≡ join X Y - join≡Susp = sym A□○≡Σ ∙ 3x3-lemma smash-span ∙ A○□≡join - + Susp≡join : Susp (X∙ ⋀ Y∙) ≡ join X Y + Susp≡join = sym A□○≡Σ ∙ 3x3-lemma smash-span ∙ A○□≡join