tweak

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