open import 1Lab.Path.Reasoning
open import 1Lab.Prelude

open import Algebra.Group.Cat.FinitelyComplete
open import Algebra.Group.Instances.Integers
open import Algebra.Group.Cat.Base
open import Algebra.Group.Homotopy
open import Algebra.Group

open import Data.Set.Truncation
open import Data.Int.Universal
open import Data.Bool
open import Data.Int

module Homotopy.Space.Circle where

private variable
  ℓ ℓ' : Level
  X : Type ℓ

Spaces: The circle🔗

The first example of nontrivial space one typically encounters when studying synthetic homotopy theory is the circle: it is, in a sense, the perfect space to start with, having exactly one nontrivial path space, which is a free group, and the simplest nontrivial free group at that: the integers.

data S¹ : Type where
  base : S¹
  loop : base ≡ base

S¹∙ : Type∙ lzero
S¹∙ = S¹ , base

Diagrammatically, we can picture the circle as being the $\infty \text{-groupoid}$ generated by the following diagram:

In type theory with K, the circle is exactly the same type as ⊤. However, with univalence, it can be shown that the circle has at least two different paths:

_ = ⊤

möbius : S¹ → Type
möbius base = Bool
möbius (loop i) = ua not≃ i

When pattern matching on the circle, we are asked to provide a basepoint b and a path l : b ≡ b, as can be seen in the definition above. To make it clearer, we can also define a recursion principle:

S¹-rec : ∀ {ℓ} {A : Type ℓ} (b : A) (l : b ≡ b) → S¹ → A
S¹-rec b l base     = b
S¹-rec b l (loop i) = l i

S¹-elim : ∀ {ℓ} {A : S¹ → Type ℓ} (b : A base) (l : PathP (λ i → A (loop i)) b b)
        → ∀ s → A s
S¹-elim b l base     = b
S¹-elim b l (loop i) = l i

We call the map möbius a double cover of the circle, since the fibre at each point is a discrete space with two elements. It has an action by the fundamental group of the circle, which has the effect of negating the “parity” of the path. In fact, we can use möbius to show that loop is not refl:

parity : base ≡ base → Bool
parity l = subst möbius l true

_ : parity refl ≡ true
_ = refl

_ : parity loop ≡ false
_ = refl

refl≠loop : ¬ refl ≡ loop
refl≠loop path = true≠false (ap parity path)

The circle is also useful as a source of counterexamples: we can prove that there is an inhabitant of (x : S¹) → x ≡ x which is not constantly refl.

always-loop : (x : S¹) → x ≡ x
always-loop = S¹-elim loop (double-connection loop loop)

Fundamental group🔗

We will now calculate that the first loop space of the circle at the basepoint is a type of integers, i.e. it satisfies the universal property of the integers. First, we generalise the construction of möbius to turn an equivalence on an arbitrary type into a type family over S¹. Transport over this family will give the universal map $\Omega S^1\to X$ associated with an equivalence $e:X\simeq X$ and basepoint $x_0:X\text{.}$

equiv→family : X ≃ X → S¹ → Type _
equiv→family {X = X} eqv base = X
equiv→family eqv (loop i)     = ua eqv i

We will later need the “action” associated with an equivalence valued at a path with free endpoint $y:S^1\text{.}$ Taking $y=\mathrm{base}$ recovers a more vanilla notion of “action on $X$”.

equiv→action : ∀ {y} (e : X ≃ X) → base ≡ y → X → equiv→family e y
equiv→action e p x = subst (equiv→family e) p x

_ : X ≃ X → base ≡ base → X → X
_ = equiv→action {y = base}

open Integers
interleaved mutual

The first thing we will do is assume an elimination principle for $\Omega S^1\text{,}$ which will be used in showing uniqueness of the universal map $\Omega S^1\to X$ associated to an equivalence $e:X\simeq X\text{.}$ We must also equip $\Omega S^1$ with an auto-equivalence, which corresponds in some way to taking successors: since loop corresponds to “the number 1”, the equivalence we go with is thus “adding 1”: postcomposition with the loop.

  ΩS¹-elim
    : ∀ {ℓ} (P : Path S¹ base base → Type ℓ)
    → (pr : P refl)
    → (pl : P ≃[ ∙-post-equiv loop ] P)
    → ∀ x → P x

  private
    rotΩS¹ : (base ≡ base) ≃ (base ≡ base)
    rotΩS¹ = ∙-post-equiv {x = base} loop

  ΩS¹-integers : Integers (Path S¹ base base)
  ΩS¹-integers .point   = refl
  ΩS¹-integers .rotate  = rotΩS¹

It is easy to see that transporting the basepoint along the family associated to an automorphism of $X$ commutes with our chosen automorphism of $\Omega S^1\text{:}$ modulo a tactic application, it is refl.

  ΩS¹-integers .map-out        x e l = equiv→action e l x
  ΩS¹-integers .map-out-point  x e   = Regularity.precise! refl
  ΩS¹-integers .map-out-rotate x e l = Regularity.precise! refl

The difficult part of the proof is showing that equiv→action is the unique map $\Omega S^1\to X$ with these properties. We will show this is the case assuming first that we have an elimination principle for $\Omega S^1\text{.}$

  ΩS¹-integers .map-out-unique f {p} {r} frefl floop = ΩS¹-elim _
    (Regularity.precise! frefl) $ over-left→over rotΩS¹ λ a →
      (f a ≡ go a)                    ≃⟨ ap-equiv r ⟩
      (r .fst (f a) ≡ r .fst (go a))  ≃⟨ ∙-pre-equiv (floop a) ⟩
      (f (a ∙ loop) ≡ r .fst (go a))  ≃⟨ ∙-post-equiv (Regularity.precise! refl) ⟩
      (f (a ∙ loop) ≡ go (a ∙ loop))  ≃∎
    where
      go : _ → _
      go l = equiv→action r l p

Loop induction🔗

We must now show the elimination principle for $\Omega S^1$ that was promised above. Note that, while this is a path type, both of the endpoints are fixed (here, to be constructors), so we can not directly use path induction. Instead, we will mimic the construction of induction from initiality, turning our induction methods into a total algebra ${\sum }_{x:\Omega S^1}P(x)\text{,}$ which can be mapped into universally.

Applying the universal map at $l:\Omega S^1$ then gives us a pair of an index $l^{\prime }:\Omega S^1$ and a proof in $P(l^{\prime })\text{.}$ If we have a proper initial object, we could then show that the composite $$\Omega S^1\to \left(\sum _{x:\Omega S^1}P(x)\right)\stackrel{{\pi }_1}{\to }\Omega S^1$$ which defines $l^{\prime }$ is an algebra map $\Omega S^1\to \Omega S^1\text{,}$ so it must be the identity; thus $l^{\prime }=l$ and we have the desired $P(l)\text{.}$ Here, however, we’re trying to show initiality, so we’ll need a hand-crafted coherence.

We note that the induction methods for ΩS¹-elim fit together into a basepoint and auto-equivalence of the type ${\sum }_{l:\Omega S^1}P(l)\text{.}$ The family associated to this action will be called totl.

  ΩS¹-elim P pr pl l = subst P (pathβ base l) attempt where
    totl : S¹ → Type _
    totl = equiv→family (over→total rotΩS¹ pl)

By rotating the basepoint (given by the method $\mathrm{pr}:P\mathrm{refl}\text{),}$ we get a value in $P\text{,}$ but its type appears to be way off. Essentially, to show that our attempt landed in the right fibre, we would like to reduce to the case where $l=\mathrm{refl}\text{,}$ since there the index is essentially trivially correct.

    attempt : P (subst totl l (refl , pr) .fst)
    attempt = subst totl l (refl , pr) .snd

However, this statement depends critically on $l$ being a loop, preventing us from using path induction: if $l$ is instead a path $\mathrm{base}\equiv y\text{,}$ then transport takes us to a fibre of totl which is not a sigma type, hence not something we can project from. To generalise this, we must define a fibrewise transformation from totl to the based path space of $S^1\text{,}$ which, at the basepoint, is the first projection function.

This turns out to be pretty easy: using the helper function ua→ to simplify the coherence condition, we are left with filling a square with the boundary below, which we have by the definition of path composition: it is ∙-filler.

    path : ∀ y → totl y → base ≡ y
    path = S¹-elim fst $ ua→ λ _ → ∙-filler _ loop

Now we have a statement which is sufficiently general to prove by path induction: projecting the index using path from the result of applying our universal map, even at an arbitrary based path $l:\mathrm{base}\equiv y\text{,}$ is the identity function; And, by construction, when $y=\mathrm{base}\text{,}$ this statement reduces to precisely the identification between indices we were looking for.

    pathβ : ∀ y l → path y (subst totl l (refl , pr)) ≡ l
    pathβ y = J (λ y l → path y (subst totl l (refl , pr)) ≡ l)
      (transport-refl refl)

ΩS¹≃Int : (base ≡ base) ≃ Int
ΩS¹≃Int = Integers-unique ΩS¹-integers Int-integers

open Equiv ΩS¹≃Int renaming (from to loopⁿ) using ()

It immediately follows from this that the circle is a groupoid, since it is connected and its loop space is a set.

opaque
  S¹-is-groupoid : is-groupoid S¹
  S¹-is-groupoid = S¹-elim (S¹-elim
    (Equiv→is-hlevel 2 ΩS¹≃Int (hlevel 2)) prop!) prop!

instance
  H-Level-S¹ : ∀ {k} → H-Level S¹ (3 + k)
  H-Level-S¹ = basic-instance 3 S¹-is-groupoid

opaque
  loopⁿ⁺¹ : (n : Int) → loopⁿ (sucℤ n) ≡ loopⁿ n ∙ loop
  loopⁿ⁺¹ n = Int-integers .map-out-rotate refl rotΩS¹ n

By induction, we can show that this equivalence respects group composition (that is, ${\mathrm{loop}}^{a+b}\equiv {\mathrm{loop}}^a\bullet {\mathrm{loop}}^b\text{),}$ so that we have a proper isomorphism of groups.

loopⁿ-+ : (a b : Int) → loopⁿ (a +ℤ b) ≡ loopⁿ a ∙ loopⁿ b
loopⁿ-+ a = Integers.induction Int-integers
  (ap loopⁿ (+ℤ-zeror a) ∙ sym (∙-idr _))
  λ b →
    loopⁿ (a +ℤ b) ≡ loopⁿ a ∙ loopⁿ b                 ≃⟨ ap (_∙ loop) , equiv→cancellable (∙-post-equiv loop .snd) ⟩
    loopⁿ (a +ℤ b) ∙ loop ≡ (loopⁿ a ∙ loopⁿ b) ∙ loop ≃⟨ ∙-post-equiv (sym (∙-assoc _ _ _)) ⟩
    loopⁿ (a +ℤ b) ∙ loop ≡ loopⁿ a ∙ loopⁿ b ∙ loop   ≃⟨ ∙-post-equiv (ap (loopⁿ a ∙_) (sym (loopⁿ⁺¹ b))) ⟩
    loopⁿ (a +ℤ b) ∙ loop ≡ loopⁿ a ∙ loopⁿ (sucℤ b)   ≃⟨ ∙-pre-equiv (loopⁿ⁺¹ (a +ℤ b)) ⟩
    loopⁿ (sucℤ (a +ℤ b)) ≡ loopⁿ a ∙ loopⁿ (sucℤ b)   ≃⟨ ∙-pre-equiv (ap loopⁿ (+ℤ-sucr a b)) ⟩
    loopⁿ (a +ℤ sucℤ b) ≡ loopⁿ a ∙ loopⁿ (sucℤ b)     ≃∎

π₁S¹≡ℤ : π₁Groupoid.π₁ S¹∙ S¹-is-groupoid ≡ ℤ
π₁S¹≡ℤ = sym $ ∫-Path
  (∫hom (Equiv.from ΩS¹≃Int)
    (record { pres-⋆ = loopⁿ-+ }))
  ((ΩS¹≃Int e⁻¹) .snd)

Furthermore, since the loop space of the circle is a set, we automatically get that all of its higher homotopy groups are trivial.

Ωⁿ⁺²S¹-is-contr : ∀ n → is-contr ⌞ Ωⁿ (2 + n) S¹∙ ⌟
Ωⁿ⁺²S¹-is-contr zero = is-prop∙→is-contr (hlevel 1) refl
Ωⁿ⁺²S¹-is-contr (suc n) = Path-is-hlevel 0 (Ωⁿ⁺²S¹-is-contr n)

πₙ₊₂S¹≡0 : ∀ n → πₙ₊₁ (suc n) S¹∙ ≡ Zero-group {lzero}
πₙ₊₂S¹≡0 n = ∫-Path
  (Zero-group-is-terminal _ .centre)
  (is-contr→≃ (is-contr→∥-∥₀-is-contr (Ωⁿ⁺²S¹-is-contr n)) (hlevel 0) .snd)