The circle

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Julian KG, fernabnor, louismntnu and maybemabeline.

Created on 2022-03-02.
Last modified on 2023-10-03.

module synthetic-homotopy-theory.circle where
Imports 
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 higher-group-theory.higher-groups

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

Postulates

postulate 𝕊¹ : UU lzero

postulate base-𝕊¹ : 𝕊¹

postulate loop-𝕊¹ : Id base-𝕊¹ base-𝕊¹

free-loop-𝕊¹ : free-loop 𝕊¹
pr1 free-loop-𝕊¹ = base-𝕊¹
pr2 free-loop-𝕊¹ = loop-𝕊¹

𝕊¹-Pointed-Type : Pointed-Type lzero
pr1 𝕊¹-Pointed-Type = 𝕊¹
pr2 𝕊¹-Pointed-Type = base-𝕊¹

postulate ind-𝕊¹ : {l : Level} → induction-principle-circle l free-loop-𝕊¹

Properties

The dependent universal property of the circle

dependent-universal-property-𝕊¹ :
  {l : Level} → dependent-universal-property-circle l free-loop-𝕊¹
dependent-universal-property-𝕊¹ =
  dependent-universal-property-induction-principle-circle free-loop-𝕊¹ ind-𝕊¹

uniqueness-dependent-universal-property-𝕊¹ :
  {l : Level} {P : 𝕊¹ → UU l} (k : free-dependent-loop free-loop-𝕊¹ P) →
  is-contr
    ( Σ ( (x : 𝕊¹) → P x)
        ( λ h →
          Eq-free-dependent-loop free-loop-𝕊¹ P
            ( ev-free-loop-Π free-loop-𝕊¹ P h) k))
uniqueness-dependent-universal-property-𝕊¹ {l} {P} =
  uniqueness-dependent-universal-property-circle
    free-loop-𝕊¹
    dependent-universal-property-𝕊¹

module _
  {l : Level} (P : 𝕊¹ → UU l) (p0 : P base-𝕊¹) (α : Id (tr P loop-𝕊¹ p0) p0)
  where

  Π-𝕊¹ : UU l
  Π-𝕊¹ =
    Σ ( (x : 𝕊¹) → P x)
      ( λ h →
        Eq-free-dependent-loop free-loop-𝕊¹ P
          ( ev-free-loop-Π free-loop-𝕊¹ P h) (pair p0 α))

  apply-dependent-universal-property-𝕊¹ : Π-𝕊¹
  apply-dependent-universal-property-𝕊¹ =
    center (uniqueness-dependent-universal-property-𝕊¹ (pair p0 α))

  function-apply-dependent-universal-property-𝕊¹ : (x : 𝕊¹) → P x
  function-apply-dependent-universal-property-𝕊¹ =
    pr1 apply-dependent-universal-property-𝕊¹

  base-dependent-universal-property-𝕊¹ :
    Id (function-apply-dependent-universal-property-𝕊¹ base-𝕊¹) p0
  base-dependent-universal-property-𝕊¹ =
    pr1 (pr2 apply-dependent-universal-property-𝕊¹)

  loop-dependent-universal-property-𝕊¹ :
    Id
      ( apd function-apply-dependent-universal-property-𝕊¹ loop-𝕊¹ ∙
        base-dependent-universal-property-𝕊¹)
      ( ap (tr P loop-𝕊¹) base-dependent-universal-property-𝕊¹ ∙ α)
  loop-dependent-universal-property-𝕊¹ =
    pr2 (pr2 apply-dependent-universal-property-𝕊¹)

The universal property of the circle

universal-property-𝕊¹ :
  {l : Level} → universal-property-circle l free-loop-𝕊¹
universal-property-𝕊¹ =
  universal-property-dependent-universal-property-circle
    free-loop-𝕊¹
    dependent-universal-property-𝕊¹

uniqueness-universal-property-𝕊¹ :
  {l : Level} {X : UU l} (α : free-loop X) →
  is-contr
    ( Σ ( 𝕊¹ → X)
        ( λ h → Eq-free-loop (ev-free-loop free-loop-𝕊¹ X h) α))
uniqueness-universal-property-𝕊¹ {l} {X} =
  uniqueness-universal-property-circle free-loop-𝕊¹ universal-property-𝕊¹ X

module _
  {l : Level} {X : UU l} (x : X) (α : Id x x)
  where

  Map-𝕊¹ : UU l
  Map-𝕊¹ =
    Σ ( 𝕊¹ → X)
      ( λ h → Eq-free-loop (ev-free-loop free-loop-𝕊¹ X h) (pair x α))

  apply-universal-property-𝕊¹ : Map-𝕊¹
  apply-universal-property-𝕊¹ =
    center (uniqueness-universal-property-𝕊¹ (pair x α))

  map-apply-universal-property-𝕊¹ : 𝕊¹ → X
  map-apply-universal-property-𝕊¹ =
    pr1 apply-universal-property-𝕊¹

  base-universal-property-𝕊¹ :
    Id (map-apply-universal-property-𝕊¹ base-𝕊¹) x
  base-universal-property-𝕊¹ =
    pr1 (pr2 apply-universal-property-𝕊¹)

  loop-universal-property-𝕊¹ :
    Id
      ( ap map-apply-universal-property-𝕊¹ loop-𝕊¹ ∙
        base-universal-property-𝕊¹)
      ( base-universal-property-𝕊¹ ∙ α)
  loop-universal-property-𝕊¹ =
    pr2 (pr2 apply-universal-property-𝕊¹)

The circle is 0-connected

mere-eq-𝕊¹ : (x y : 𝕊¹) → mere-eq x y
mere-eq-𝕊¹ =
  function-apply-dependent-universal-property-𝕊¹
    ( λ x → (y : 𝕊¹) → mere-eq x y)
    ( function-apply-dependent-universal-property-𝕊¹
      ( mere-eq base-𝕊¹)
      ( refl-mere-eq base-𝕊¹)
      ( eq-is-prop is-prop-type-trunc-Prop))
    ( eq-is-prop (is-prop-Π (λ y → is-prop-type-trunc-Prop)))

is-0-connected-𝕊¹ : is-0-connected 𝕊¹
is-0-connected-𝕊¹ = is-0-connected-mere-eq base-𝕊¹ (mere-eq-𝕊¹ base-𝕊¹)

The circle as a higher group

𝕊¹-∞-Group : ∞-Group lzero
pr1 𝕊¹-∞-Group = 𝕊¹-Pointed-Type
pr2 𝕊¹-∞-Group = is-0-connected-𝕊¹

The circle is equivalent to the 1-sphere

The 1-sphere is defined as the suspension of the 0-sphere. We may understand this as the 1-sphere having two points N and S and two identifications (meridians) e, w : N = S between them. The following shows that the 1-sphere and the circle are equivalent.

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.

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.

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.

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.

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

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

Recent changes