module Homotopy.Space.Circle where

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 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

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 associated with an equivalence and basepoint

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 Taking recovers a more vanilla notion of “action on ”.

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}

The first thing we will do is assume an elimination principle for which will be used in showing uniqueness of the universal map associated to an equivalence We must also equip 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 commutes with our chosen automorphism of 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 with these properties. We will show this is the case assuming first that we have an elimination principle for

  Ω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 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 which can be mapped into universally.

Applying the universal map at then gives us a pair of an index and a proof in If we have a proper initial object, we could then show that the composite which defines is an algebra map so it must be the identity; thus and we have the desired 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 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 we get a value in 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 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 being a loop, preventing us from using path induction: if is instead a path 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 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 is the identity function; And, by construction, when 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!

By induction, we can show that this equivalence respects group composition (that is, 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)