From d3e699f683f36404b41a8841ed7d27da8f0c0812 Mon Sep 17 00:00:00 2001 From: ecavallo Date: Fri, 22 Oct 2021 18:52:34 +0200 Subject: [PATCH] =?UTF-8?q?fix=20merge=20conflict=20from=20=E2=88=99Susp?= =?UTF-8?q?=20=E2=86=92=20Susp=E2=88=99=20renaming?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Cubical/HITs/Susp/LoopAdjunction.agda | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/Cubical/HITs/Susp/LoopAdjunction.agda b/Cubical/HITs/Susp/LoopAdjunction.agda index 7bd14996b4..91be404b7b 100644 --- a/Cubical/HITs/Susp/LoopAdjunction.agda +++ b/Cubical/HITs/Susp/LoopAdjunction.agda @@ -27,15 +27,15 @@ private Ω∙ (suc (suc n)) X = Ω∙ 1 (Ω∙ (suc n) X) ΣX→∙YEquiv : ((X , x₀) : Pointed ℓ) ((Y , y₀) : Pointed ℓ') - → (∙Susp X →∙ (Y , y₀)) ≃ (Σ[ y ∈ Y ] (X → (y₀ ≡ y))) + → (Susp∙ X →∙ (Y , y₀)) ≃ (Σ[ y ∈ Y ] (X → (y₀ ≡ y))) ΣX→∙YEquiv (X , x₀) (Y , y₀) = isoToEquiv (iso left→right right→left right→left→right left→right→left) where - left→right : (∙Susp X →∙ (Y , y₀)) → Σ[ y ∈ Y ] (X → (y₀ ≡ y)) + left→right : (Susp∙ X →∙ (Y , y₀)) → Σ[ y ∈ Y ] (X → (y₀ ≡ y)) left→right (f , b) .fst = f south left→right (f , b) .snd x = sym b ∙ cong f (merid x) - right→left : (Σ[ y ∈ Y ] (X → (y₀ ≡ y))) → (∙Susp X →∙ (Y , y₀)) + right→left : (Σ[ y ∈ Y ] (X → (y₀ ≡ y))) → (Susp∙ X →∙ (Y , y₀)) right→left (y , g) .fst north = y₀ right→left (y , g) .fst south = y right→left (y , g) .fst (merid x i) = g x i @@ -45,7 +45,7 @@ private right→left→right (y , g) i .fst = y right→left→right (y , g) i .snd x = lUnit (g x) (~ i) - left→right→left : (f : ∙Susp X →∙ (Y , y₀)) → right→left (left→right f) ≡ f + left→right→left : (f : Susp∙ X →∙ (Y , y₀)) → right→left (left→right f) ≡ f left→right→left (f , b) i .fst north = b (~ i) left→right→left (f , b) i .fst south = f south left→right→left (f , b) i .fst (merid x j) = @@ -109,5 +109,5 @@ X→∙ΩYEquiv (X , x₀) (Y , y₀) = (bottom (f , b) i j k) {- The Main Theorem -} -ΣΩAdjunction : ((X , x₀) : Pointed ℓ) (Y : Pointed ℓ') → (∙Susp X →∙ Y) ≃ ((X , x₀) →∙ Ω∙ 1 Y) +ΣΩAdjunction : ((X , x₀) : Pointed ℓ) (Y : Pointed ℓ') → (Susp∙ X →∙ Y) ≃ ((X , x₀) →∙ Ω∙ 1 Y) ΣΩAdjunction X Y = compEquiv (ΣX→∙YEquiv X Y) (invEquiv (X→∙ΩYEquiv X Y))