From 1fb5dc5cdf267ede3e8b770cb3c2dc589a1fa2e2 Mon Sep 17 00:00:00 2001
From: maybemabeline <142519092+maybemabeline@users.noreply.github.com>
Date: Sat, 16 Sep 2023 22:32:19 +0200
Subject: [PATCH] Equivalence between the first sphere and the circle (#776)

Co-authored-by: Egbert Rijke <e.m.rijke@gmail.com>
---
 src/foundation-core/homotopies.lagda.md       |   8 +
 src/foundation/path-algebra.lagda.md          |   2 +-
 src/synthetic-homotopy-theory/circle.lagda.md | 396 ++++++++++++++++++
 ...nt-universal-property-suspensions.lagda.md |   4 +-
 .../spheres.lagda.md                          |   6 +
 .../suspension-structures.lagda.md            |   2 +-
 6 files changed, 413 insertions(+), 5 deletions(-)

diff --git a/src/foundation-core/homotopies.lagda.md b/src/foundation-core/homotopies.lagda.md
index e7634247d9..a8a2adcfe1 100644
--- a/src/foundation-core/homotopies.lagda.md
+++ b/src/foundation-core/homotopies.lagda.md
@@ -72,6 +72,14 @@ map-compute-dependent-identification-eq-value-id-id :
   dependent-identification (eq-value id id) p q r
 map-compute-dependent-identification-eq-value-id-id refl q r s =
   inv (s ∙ right-unit)
+
+map-compute-dependent-identification-eq-value-comp-id :
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (g : B → A) (f : A → B) {a b : A}
+  (p : a ＝ b) (q : eq-value (g ∘ f) id a) (r : eq-value (g ∘ f) id b) →
+  coherence-square-identifications (ap g (ap f p)) r q p →
+  dependent-identification (eq-value (g ∘ f) id) p q r
+map-compute-dependent-identification-eq-value-comp-id g f refl q r s =
+  inv (s ∙ right-unit)
 ```
 
 ### Homotopies
diff --git a/src/foundation/path-algebra.lagda.md b/src/foundation/path-algebra.lagda.md
index c5b9f15133..a649874445 100644
--- a/src/foundation/path-algebra.lagda.md
+++ b/src/foundation/path-algebra.lagda.md
@@ -620,7 +620,7 @@ interchange-y-z-concat-Id³ refl refl refl refl = inv right-unit
 
 ## Properties of 4-paths
 
-The pattern for concatination of 1, 2, and 3-paths continues. There are four
+The pattern for concatenation of 1, 2, and 3-paths continues. There are four
 ways to concatenate in quadruple identity types. We name the three non-standard
 concatenations in quadruple identity types `i`-, `j`-, and `k`-concatenation,
 after the standard names for the quaternions `i`, `j`, and `k`.
diff --git a/src/synthetic-homotopy-theory/circle.lagda.md b/src/synthetic-homotopy-theory/circle.lagda.md
index 71067c794a..78e6e2e041 100644
--- a/src/synthetic-homotopy-theory/circle.lagda.md
+++ b/src/synthetic-homotopy-theory/circle.lagda.md
@@ -10,19 +10,33 @@ module synthetic-homotopy-theory.circle where
 open import foundation.0-connected-types
 open import foundation.action-on-identifications-dependent-functions
 open import foundation.action-on-identifications-functions
+open import foundation.commuting-squares-of-identifications
 open import foundation.contractible-types
+open import foundation.coproduct-types
+open import foundation.dependent-identifications
 open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.mere-equality
+open import foundation.path-algebra
 open import foundation.propositional-truncations
 open import foundation.propositions
+open import foundation.retractions
+open import foundation.sections
 open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
 open import structured-types.pointed-types
 
+open import synthetic-homotopy-theory.dependent-suspension-structures
 open import synthetic-homotopy-theory.free-loops
+open import synthetic-homotopy-theory.spheres
+open import synthetic-homotopy-theory.suspension-structures
+open import synthetic-homotopy-theory.suspensions-of-types
 open import synthetic-homotopy-theory.universal-property-circle
+
+open import univalent-combinatorics.standard-finite-types
 ```
 
 </details>
@@ -167,3 +181,385 @@ mere-eq-𝕊¹ =
 is-0-connected-𝕊¹ : is-0-connected 𝕊¹
 is-0-connected-𝕊¹ = is-0-connected-mere-eq base-𝕊¹ (mere-eq-𝕊¹ base-𝕊¹)
 ```
+
+### The circle is equivalent to the 1-sphere
+
+The [1-sphere](synthetic-homotopy-theory.spheres.md) is defined as the
+[suspension](synthetic-homotopy-theory.suspensions-of-types.md) of the
+[0-sphere](synthetic-homotopy-theory.spheres.md). We may understand this as the
+1-sphere having two points `N` and `S` and two
+[identifications](foundation-core.identity-types.md) (meridians) `e, w : N = S`
+between them. The following shows that the 1-sphere and the circle are
+[equivalent](foundation-core.equivalences.md).
+
+#### The map from the circle to the 1-sphere
+
+The map from the circle to the 1-sphere is defined by mapping the basepoint to
+`N` and the loop to the composite of `e` and the inverse of `w`, which forms a
+loop at `N`. The choice of which meridian to start with is arbitrary, but
+informs the rest of the construction hereafter.
+
+```agda
+north-sphere-1-loop : Id (north-sphere 1) (north-sphere 1)
+north-sphere-1-loop =
+  ( meridian-sphere 0 (zero-Fin 1)) ∙
+  ( inv (meridian-sphere 0 (one-Fin 1)))
+
+sphere-1-circle : 𝕊¹ → sphere 1
+sphere-1-circle =
+  map-apply-universal-property-𝕊¹ (north-sphere 1) north-sphere-1-loop
+
+sphere-1-circle-base-𝕊¹-eq-north-sphere-1 :
+  Id (sphere-1-circle base-𝕊¹) (north-sphere 1)
+sphere-1-circle-base-𝕊¹-eq-north-sphere-1 =
+  base-universal-property-𝕊¹ (north-sphere 1) north-sphere-1-loop
+
+sphere-1-circle-base-𝕊¹-eq-south-sphere-1 :
+  Id (sphere-1-circle base-𝕊¹) (south-sphere 1)
+sphere-1-circle-base-𝕊¹-eq-south-sphere-1 =
+  ( sphere-1-circle-base-𝕊¹-eq-north-sphere-1) ∙
+  ( meridian-sphere 0 (one-Fin 1))
+```
+
+#### The map from the 1-sphere to the circle
+
+The map from the 1-sphere to the circle is defined by mapping both `N` and `S`
+to the basepoint, `e` to the loop and `w` to `refl` at the basepoint. Were we to
+map both meridians to the loop, we would wrap the 1-sphere twice around the
+circle, which would not form an equivalence.
+
+```agda
+map-sphere-0-eq-base-𝕊¹ : (sphere 0) → base-𝕊¹ ＝ base-𝕊¹
+map-sphere-0-eq-base-𝕊¹ (inl n) = loop-𝕊¹
+map-sphere-0-eq-base-𝕊¹ (inr n) = refl
+
+suspension-structure-sphere-0-𝕊¹ :
+  suspension-structure (sphere 0) 𝕊¹
+pr1 suspension-structure-sphere-0-𝕊¹ = base-𝕊¹
+pr1 (pr2 suspension-structure-sphere-0-𝕊¹) = base-𝕊¹
+pr2 (pr2 suspension-structure-sphere-0-𝕊¹) = map-sphere-0-eq-base-𝕊¹
+
+circle-sphere-1 : sphere 1 → 𝕊¹
+circle-sphere-1 =
+  map-inv-up-suspension
+    ( sphere 0)
+    ( 𝕊¹)
+    ( suspension-structure-sphere-0-𝕊¹)
+
+circle-sphere-1-north-sphere-1-eq-base-𝕊¹ :
+  Id (circle-sphere-1 (north-sphere 1)) base-𝕊¹
+circle-sphere-1-north-sphere-1-eq-base-𝕊¹ =
+  up-suspension-north-suspension
+    ( sphere 0)
+    ( 𝕊¹)
+    ( suspension-structure-sphere-0-𝕊¹)
+
+circle-sphere-1-south-sphere-1-eq-base-𝕊¹ :
+  Id (circle-sphere-1 (south-sphere 1)) base-𝕊¹
+circle-sphere-1-south-sphere-1-eq-base-𝕊¹ =
+  up-suspension-south-suspension
+    ( sphere 0)
+    ( 𝕊¹)
+    ( suspension-structure-sphere-0-𝕊¹)
+```
+
+#### The map from the circle to the 1-sphere has a section
+
+Some care needs to be taken when proving this part of the equivalence. The point
+`N` is mapped to the basepoint and then back to `N`, but so is the point `S`. It
+needs to be further identified back with `S` using the meridian `w`. The
+meridian `w` is thus mapped to `refl` and then back to `w ∙ refl = w`, while the
+meridian `e` is mapped to the loop and then back to `w ∙ w⁻¹∙ e = e`.
+
+```agda
+sphere-1-circle-sphere-1-north-sphere-1 :
+    ( sphere-1-circle (circle-sphere-1 (north-sphere 1))) ＝ ( north-sphere 1)
+sphere-1-circle-sphere-1-north-sphere-1 =
+  ( ap sphere-1-circle circle-sphere-1-north-sphere-1-eq-base-𝕊¹) ∙
+  ( sphere-1-circle-base-𝕊¹-eq-north-sphere-1)
+
+sphere-1-circle-sphere-1-south-sphere-1 :
+    ( sphere-1-circle (circle-sphere-1 (south-sphere 1))) ＝ ( south-sphere 1)
+sphere-1-circle-sphere-1-south-sphere-1 =
+  ( ap sphere-1-circle circle-sphere-1-south-sphere-1-eq-base-𝕊¹) ∙
+  ( sphere-1-circle-base-𝕊¹-eq-south-sphere-1)
+
+apply-up-suspension-meridian-suspension-sphere-1-circle-sphere-1 :
+  ( n : Fin 2) →
+  coherence-square-identifications
+    ( ap sphere-1-circle (ap circle-sphere-1 (meridian-suspension n)))
+    ( sphere-1-circle-sphere-1-south-sphere-1)
+    ( ap
+      ( sphere-1-circle)
+      ( ( circle-sphere-1-north-sphere-1-eq-base-𝕊¹) ∙
+        ( map-sphere-0-eq-base-𝕊¹ n)))
+    ( sphere-1-circle-base-𝕊¹-eq-south-sphere-1)
+apply-up-suspension-meridian-suspension-sphere-1-circle-sphere-1 n =
+  ( inv
+    ( assoc
+      ( ap sphere-1-circle (ap circle-sphere-1 (meridian-suspension n)))
+      ( ap sphere-1-circle circle-sphere-1-south-sphere-1-eq-base-𝕊¹)
+      ( sphere-1-circle-base-𝕊¹-eq-south-sphere-1))) ∙
+  ( identification-right-whisk
+    ( inv
+      ( ap-concat
+        ( sphere-1-circle)
+        ( ap circle-sphere-1 (meridian-sphere 0 n))
+        ( circle-sphere-1-south-sphere-1-eq-base-𝕊¹)))
+    ( sphere-1-circle-base-𝕊¹-eq-south-sphere-1)) ∙
+  ( ap
+    ( λ x →
+      ( ap sphere-1-circle x) ∙
+      ( sphere-1-circle-base-𝕊¹-eq-south-sphere-1))
+    ( up-suspension-meridian-suspension
+      ( sphere 0)
+      ( 𝕊¹)
+      ( suspension-structure-sphere-0-𝕊¹)
+      ( n)))
+
+apply-loop-universal-property-𝕊¹-sphere-1-circle-sphere-1 :
+  coherence-square-identifications
+    ( ap sphere-1-circle loop-𝕊¹)
+    ( sphere-1-circle-base-𝕊¹-eq-south-sphere-1)
+    ( sphere-1-circle-base-𝕊¹-eq-north-sphere-1)
+    ( meridian-sphere 0 (zero-Fin 1))
+apply-loop-universal-property-𝕊¹-sphere-1-circle-sphere-1 =
+  ( inv
+    ( assoc
+      ( ap sphere-1-circle loop-𝕊¹)
+      ( sphere-1-circle-base-𝕊¹-eq-north-sphere-1)
+      ( meridian-sphere 0 (one-Fin 1)))) ∙
+  ( identification-right-whisk
+    ( loop-universal-property-𝕊¹
+      ( north-sphere 1)
+      ( north-sphere-1-loop))
+    ( meridian-sphere 0 (one-Fin 1))) ∙
+  ( assoc
+    ( sphere-1-circle-base-𝕊¹-eq-north-sphere-1)
+    ( north-sphere-1-loop)
+    ( meridian-sphere 0 (one-Fin 1))) ∙
+  ( identification-left-whisk
+    ( sphere-1-circle-base-𝕊¹-eq-north-sphere-1)
+    ( is-section-right-concat-inv
+      ( meridian-sphere 0 (zero-Fin 1))
+      ( meridian-sphere 0 (one-Fin 1))))
+
+map-sphere-1-circle-sphere-1-meridian :
+  ( n : Fin 2) →
+  ( dependent-identification
+    ( λ x → (sphere-1-circle (circle-sphere-1 x)) ＝ x)
+    ( meridian-suspension-structure
+      ( suspension-structure-suspension (Fin 2))
+      ( n))
+    ( sphere-1-circle-sphere-1-north-sphere-1)
+    ( sphere-1-circle-sphere-1-south-sphere-1))
+map-sphere-1-circle-sphere-1-meridian (inl (inr n)) =
+  map-compute-dependent-identification-eq-value-comp-id
+    ( sphere-1-circle)
+    ( circle-sphere-1)
+    ( meridian-sphere 0 (inl (inr n)))
+    ( sphere-1-circle-sphere-1-north-sphere-1)
+    ( sphere-1-circle-sphere-1-south-sphere-1)
+    ( ( apply-up-suspension-meridian-suspension-sphere-1-circle-sphere-1
+        ( inl (inr n))) ∙
+      ( identification-right-whisk
+        ( ap-concat
+          ( sphere-1-circle)
+          ( circle-sphere-1-north-sphere-1-eq-base-𝕊¹)
+          ( loop-𝕊¹))
+        ( sphere-1-circle-base-𝕊¹-eq-south-sphere-1)) ∙
+      ( assoc
+        ( ap sphere-1-circle (circle-sphere-1-north-sphere-1-eq-base-𝕊¹))
+        ( ap sphere-1-circle loop-𝕊¹)
+        ( sphere-1-circle-base-𝕊¹-eq-south-sphere-1)) ∙
+      ( identification-left-whisk
+        ( ap sphere-1-circle (circle-sphere-1-north-sphere-1-eq-base-𝕊¹))
+        ( apply-loop-universal-property-𝕊¹-sphere-1-circle-sphere-1)) ∙
+      ( inv
+        ( assoc
+          ( ap sphere-1-circle (circle-sphere-1-north-sphere-1-eq-base-𝕊¹))
+          ( sphere-1-circle-base-𝕊¹-eq-north-sphere-1)
+          ( meridian-sphere 0 (zero-Fin 1)))))
+map-sphere-1-circle-sphere-1-meridian (inr n) =
+  map-compute-dependent-identification-eq-value-comp-id
+    ( sphere-1-circle)
+    ( circle-sphere-1)
+    ( meridian-sphere 0 (inr n))
+    ( sphere-1-circle-sphere-1-north-sphere-1)
+    ( sphere-1-circle-sphere-1-south-sphere-1)
+    ( ( apply-up-suspension-meridian-suspension-sphere-1-circle-sphere-1
+        ( inr n)) ∙
+      ( ap
+        ( λ x →
+          ( ap sphere-1-circle x) ∙
+          ( sphere-1-circle-base-𝕊¹-eq-south-sphere-1))
+        ( right-unit {p = circle-sphere-1-north-sphere-1-eq-base-𝕊¹})) ∙
+      ( inv
+        ( assoc
+          ( ap sphere-1-circle circle-sphere-1-north-sphere-1-eq-base-𝕊¹)
+          ( sphere-1-circle-base-𝕊¹-eq-north-sphere-1)
+          ( meridian-sphere 0 (one-Fin 1)))))
+
+dependent-suspension-structure-sphere-1-circle-sphere-1 :
+  dependent-suspension-structure
+    ( λ x → (sphere-1-circle (circle-sphere-1 x)) ＝ x)
+    ( suspension-structure-suspension (Fin 2))
+pr1 dependent-suspension-structure-sphere-1-circle-sphere-1 =
+  sphere-1-circle-sphere-1-north-sphere-1
+pr1 (pr2 dependent-suspension-structure-sphere-1-circle-sphere-1) =
+  sphere-1-circle-sphere-1-south-sphere-1
+pr2 (pr2 dependent-suspension-structure-sphere-1-circle-sphere-1) =
+  map-sphere-1-circle-sphere-1-meridian
+
+sphere-1-circle-sphere-1 : section sphere-1-circle
+pr1 sphere-1-circle-sphere-1 = circle-sphere-1
+pr2 sphere-1-circle-sphere-1 =
+  map-inv-dependent-up-suspension
+    ( λ x → (sphere-1-circle (circle-sphere-1 x)) ＝ x)
+    ( dependent-suspension-structure-sphere-1-circle-sphere-1)
+```
+
+#### The map from the circle to the 1-sphere has a retraction
+
+The basepoint is mapped to `N` and then back to the basepoint, while the loop is
+mapped to `w⁻¹∙ e` and then back to `refl⁻¹ ∙ loop = loop`.
+
+```agda
+circle-sphere-1-circle-base-𝕊¹ :
+  Id (circle-sphere-1 (sphere-1-circle base-𝕊¹)) base-𝕊¹
+circle-sphere-1-circle-base-𝕊¹ =
+  ( ap circle-sphere-1 sphere-1-circle-base-𝕊¹-eq-north-sphere-1) ∙
+  ( circle-sphere-1-north-sphere-1-eq-base-𝕊¹)
+
+apply-up-suspension-meridian-one-suspension-circle-sphere-1-circle :
+  coherence-square-identifications
+    ( ap circle-sphere-1 (inv (meridian-sphere 0 (one-Fin 1))))
+    ( circle-sphere-1-north-sphere-1-eq-base-𝕊¹)
+    ( refl)
+    ( circle-sphere-1-south-sphere-1-eq-base-𝕊¹)
+apply-up-suspension-meridian-one-suspension-circle-sphere-1-circle =
+  ( identification-right-whisk
+    ( ap-inv
+      ( circle-sphere-1)
+      ( meridian-suspension (one-Fin 1)))
+    ( circle-sphere-1-north-sphere-1-eq-base-𝕊¹)) ∙
+  ( inv right-unit) ∙
+  ( assoc
+    ( inv (ap circle-sphere-1 (meridian-suspension (one-Fin 1))))
+    ( circle-sphere-1-north-sphere-1-eq-base-𝕊¹)
+    ( refl)) ∙
+  ( identification-left-whisk
+    ( inv (ap circle-sphere-1 (meridian-suspension (one-Fin 1))))
+    ( inv
+      ( up-suspension-meridian-suspension
+        (sphere 0) 𝕊¹ suspension-structure-sphere-0-𝕊¹ (one-Fin 1)))) ∙
+  ( inv
+    ( assoc
+      ( inv (ap circle-sphere-1 (meridian-suspension (one-Fin 1))))
+      ( ap circle-sphere-1 (meridian-suspension (one-Fin 1)))
+      ( circle-sphere-1-south-sphere-1-eq-base-𝕊¹))) ∙
+  ( identification-right-whisk
+    ( left-inv (ap circle-sphere-1 (meridian-suspension (one-Fin 1))))
+    ( circle-sphere-1-south-sphere-1-eq-base-𝕊¹))
+
+apply-up-suspension-meridian-zero-suspension-circle-sphere-1-circle :
+  coherence-square-identifications
+    ( ap (circle-sphere-1) (north-sphere-1-loop))
+    ( circle-sphere-1-north-sphere-1-eq-base-𝕊¹)
+    ( circle-sphere-1-north-sphere-1-eq-base-𝕊¹)
+    ( loop-𝕊¹)
+apply-up-suspension-meridian-zero-suspension-circle-sphere-1-circle =
+  ( identification-right-whisk
+    ( ap-concat
+      ( circle-sphere-1)
+      ( meridian-sphere 0 (zero-Fin 1))
+      ( inv (meridian-suspension (one-Fin 1))))
+    ( circle-sphere-1-north-sphere-1-eq-base-𝕊¹)) ∙
+  ( assoc
+    ( ap circle-sphere-1 (meridian-suspension (zero-Fin 1)))
+    ( ap circle-sphere-1 (inv ( meridian-sphere 0 (one-Fin 1))))
+    ( circle-sphere-1-north-sphere-1-eq-base-𝕊¹)) ∙
+  ( identification-left-whisk
+    ( ap circle-sphere-1 (meridian-suspension (zero-Fin 1)))
+    ( apply-up-suspension-meridian-one-suspension-circle-sphere-1-circle)) ∙
+  ( up-suspension-meridian-suspension
+    ( sphere 0)
+    ( 𝕊¹)
+    ( suspension-structure-sphere-0-𝕊¹)
+    ( zero-Fin 1))
+
+circle-sphere-1-circle-loop-𝕊¹ :
+  coherence-square-identifications
+    ( ap circle-sphere-1 (ap sphere-1-circle loop-𝕊¹))
+    ( circle-sphere-1-circle-base-𝕊¹)
+    ( circle-sphere-1-circle-base-𝕊¹)
+    ( loop-𝕊¹)
+circle-sphere-1-circle-loop-𝕊¹ =
+  ( inv
+    ( assoc
+      ( ap circle-sphere-1 (ap sphere-1-circle loop-𝕊¹))
+      ( ap
+        ( circle-sphere-1)
+        ( sphere-1-circle-base-𝕊¹-eq-north-sphere-1))
+      ( circle-sphere-1-north-sphere-1-eq-base-𝕊¹)) ∙
+    ( identification-right-whisk
+      ( inv
+        ( ap-concat
+          ( circle-sphere-1)
+          ( ap sphere-1-circle loop-𝕊¹)
+          ( sphere-1-circle-base-𝕊¹-eq-north-sphere-1)))
+      ( circle-sphere-1-north-sphere-1-eq-base-𝕊¹)) ∙
+    ( identification-right-whisk
+      ( ap
+        ( ap circle-sphere-1)
+        ( loop-universal-property-𝕊¹
+          ( north-sphere 1)
+          ( north-sphere-1-loop)))
+      ( circle-sphere-1-north-sphere-1-eq-base-𝕊¹)) ∙
+    ( identification-right-whisk
+      ( ap-concat
+        ( circle-sphere-1)
+        ( sphere-1-circle-base-𝕊¹-eq-north-sphere-1)
+        ( north-sphere-1-loop))
+      ( circle-sphere-1-north-sphere-1-eq-base-𝕊¹)) ∙
+    ( assoc
+      ( ap circle-sphere-1 sphere-1-circle-base-𝕊¹-eq-north-sphere-1)
+      ( ap circle-sphere-1 north-sphere-1-loop)
+      ( circle-sphere-1-north-sphere-1-eq-base-𝕊¹)) ∙
+    ( identification-left-whisk
+      ( ap circle-sphere-1 sphere-1-circle-base-𝕊¹-eq-north-sphere-1)
+      ( apply-up-suspension-meridian-zero-suspension-circle-sphere-1-circle)) ∙
+    ( inv
+      ( assoc
+        ( ap circle-sphere-1 sphere-1-circle-base-𝕊¹-eq-north-sphere-1)
+        ( circle-sphere-1-north-sphere-1-eq-base-𝕊¹)
+        ( loop-𝕊¹))))
+
+circle-sphere-1-circle : retraction sphere-1-circle
+pr1 circle-sphere-1-circle = circle-sphere-1
+pr2 circle-sphere-1-circle =
+  function-apply-dependent-universal-property-𝕊¹
+    ( λ x → (circle-sphere-1 (sphere-1-circle x)) ＝ x)
+    ( circle-sphere-1-circle-base-𝕊¹)
+    ( map-compute-dependent-identification-eq-value-comp-id
+      ( circle-sphere-1)
+      ( sphere-1-circle)
+      ( loop-𝕊¹)
+      ( circle-sphere-1-circle-base-𝕊¹)
+      ( circle-sphere-1-circle-base-𝕊¹)
+      ( circle-sphere-1-circle-loop-𝕊¹))
+```
+
+#### The equivalence between the circle and the 1-sphere
+
+```agda
+is-equiv-sphere-1-circle : is-equiv sphere-1-circle
+pr1 is-equiv-sphere-1-circle =
+  sphere-1-circle-sphere-1
+pr2 is-equiv-sphere-1-circle =
+  circle-sphere-1-circle
+
+equiv-sphere-1-circle : 𝕊¹ ≃ sphere 1
+pr1 equiv-sphere-1-circle = sphere-1-circle
+pr2 equiv-sphere-1-circle = is-equiv-sphere-1-circle
+```
diff --git a/src/synthetic-homotopy-theory/dependent-universal-property-suspensions.lagda.md b/src/synthetic-homotopy-theory/dependent-universal-property-suspensions.lagda.md
index e4b40dc9c1..99f5716b12 100644
--- a/src/synthetic-homotopy-theory/dependent-universal-property-suspensions.lagda.md
+++ b/src/synthetic-homotopy-theory/dependent-universal-property-suspensions.lagda.md
@@ -55,9 +55,7 @@ module _
     (B : Y → UU l) → is-equiv (dependent-ev-suspension s B)
 ```
 
-#### Coherence between `dependent-ev-suspension` and
-
-`dependent-cocone-map`
+#### Coherence between `dependent-ev-suspension` and `dependent-cocone-map`
 
 ```agda
 module _
diff --git a/src/synthetic-homotopy-theory/spheres.lagda.md b/src/synthetic-homotopy-theory/spheres.lagda.md
index 724bc132f6..ff3be84437 100644
--- a/src/synthetic-homotopy-theory/spheres.lagda.md
+++ b/src/synthetic-homotopy-theory/spheres.lagda.md
@@ -9,6 +9,7 @@ module synthetic-homotopy-theory.spheres where
 ```agda
 open import elementary-number-theory.natural-numbers
 
+open import foundation.identity-types
 open import foundation.universe-levels
 
 open import synthetic-homotopy-theory.suspensions-of-types
@@ -36,4 +37,9 @@ north-sphere (succ-ℕ n) = north-suspension
 south-sphere : (n : ℕ) → sphere n
 south-sphere zero-ℕ = one-Fin 1
 south-sphere (succ-ℕ n) = south-suspension
+
+meridian-sphere :
+  (n : ℕ) → sphere n →
+  north-sphere (succ-ℕ n) ＝ south-sphere (succ-ℕ n)
+meridian-sphere n = meridian-suspension
 ```
diff --git a/src/synthetic-homotopy-theory/suspension-structures.lagda.md b/src/synthetic-homotopy-theory/suspension-structures.lagda.md
index 3e73a38685..28e806f73d 100644
--- a/src/synthetic-homotopy-theory/suspension-structures.lagda.md
+++ b/src/synthetic-homotopy-theory/suspension-structures.lagda.md
@@ -34,7 +34,7 @@ open import synthetic-homotopy-theory.cocones-under-spans
 The suspension of `X` is the [pushout](synthetic-homotopy-theory.pushouts.md) of
 the span `unit <-- X --> unit`. A
 [cocone under such a span](synthetic-homotopy-theory.dependent-cocones-under-spans.md)
-is called a `suspension-cocone'. Explicitly, a suspension cocone with nadir `Y`
+is called a `suspension-cocone`. Explicitly, a suspension cocone with nadir `Y`
 consists of functions
 
 ```text