Rename

agda · Aug 15, 2024 · b76b3e5 · b76b3e5
1 parent d5eff6f
commit b76b3e5
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 6 deletions.
diff --git a/Cubical/HITs/Join/SuspWedgeEquiv.agda b/Cubical/HITs/Join/SuspWedgeEquiv.agda
@@ -119,7 +119,7 @@ module _ {ℓ ℓ'} (X∙ @ (X , x₀) : Pointed ℓ) (Y∙ @ (Y , y₀) : Point
       e4 = invEquiv (pushoutIdfunEquiv _) ;
       H1 = λ _ → refl ;
       H3 = λ _ → refl
-    } ∙ sym (Susp≡Pushout {ℓ-max ℓ ℓ'})
+    } ∙ sym (Susp≡PushoutSusp* {ℓ-max ℓ ℓ'})
 
   join≡Susp : Susp (X∙ ⋀ Y∙) ≡ join X Y
   join≡Susp = sym A□○≡Σ ∙ 3x3-lemma smash-span ∙ A○□≡join

diff --git a/Cubical/HITs/Susp/Properties.agda b/Cubical/HITs/Susp/Properties.agda
@@ -105,12 +105,12 @@ SuspPushoutSquare ℓ' ℓ'' A = isoToIsEquiv (iso _ inverse rInv lInv)
     lInv (inr x) = refl
     lInv (push a i) = refl
 
-Susp≃Pushout : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} → Susp A ≃ Pushout _ _
-Susp≃Pushout {ℓ} {ℓ'} {ℓ''} {A} = invEquiv (_ , SuspPushoutSquare ℓ' ℓ'' A)
+Susp≃PushoutSusp* : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} → Susp A ≃ Pushout _ _
+Susp≃PushoutSusp* {ℓ} {ℓ'} {ℓ''} {A} = invEquiv (_ , SuspPushoutSquare ℓ' ℓ'' A)
 
-Susp≡Pushout : ∀ {ℓ ℓ' ℓ''} {A : Type _} → Susp A ≡ Pushout _ _
-Susp≡Pushout {ℓ} {ℓ'} {ℓ''} = ua
-  (Susp≃Pushout {ℓ-max ℓ (ℓ-max ℓ' ℓ'')} {ℓ'} {ℓ''})
+Susp≡PushoutSusp* : ∀ {ℓ ℓ' ℓ''} {A : Type _} → Susp A ≡ Pushout _ _
+Susp≡PushoutSusp* {ℓ} {ℓ'} {ℓ''} = ua
+  (Susp≃PushoutSusp* {ℓ-max ℓ (ℓ-max ℓ' ℓ'')} {ℓ'} {ℓ''})
 
 congSuspIso : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → Iso A B → Iso (Susp A) (Susp B)
 fun (congSuspIso is) = suspFun (fun is)