⚠️ This module is not part of this project and is only included for reference.
It is either part of the 1lab, the cubical library, or a built-in Agda module.
<!--
```agda
open import 1Lab.Path.Reasoning
open import 1Lab.Prelude
open import Algebra.Group.Cat.FinitelyComplete
open import Algebra.Group.Cat.Base
open import Algebra.Group.Homotopy
open import Algebra.Group.Ab
open import Algebra.Group
open import Data.Set.Truncation
open import Data.Int.Universal
open import Data.Bool
open import Data.Int
```
-->
```agda
module Homotopy.Space.Circle where
```
# Spaces: The circle {defines="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|free group construction]], and the simplest
nontrivial [[free group|free group construction]] at that: the integers.
```agda
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$-groupoid generated by the following diagram:
~~~{.quiver}
\begin{tikzpicture}
\node[draw,circle,label=below:{$\rm{base}$},fill,outer sep=0.1cm, inner sep=0pt, minimum size=0.1cm] (a0) at (0, -1) {};
\draw[->] (0, 0) circle (1cm);
\node[] (loop) at (0, 0) {$\rm{loop}\ i$};
\end{tikzpicture}
~~~
In type theory with K, the circle is exactly the same type as
`⊤`{.Agda}. However, with `univalence`{.Agda ident=ua}, it can be shown
that the circle has at least two different paths:
<!--
```
_ = ⊤
```
-->
```agda
möbius : S¹ → Type
möbius base = Bool
möbius (loop i) = ua (not , not-is-equiv) 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:
```agda
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
```
<!--
```agda
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`{.Agda} 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`{.Agda}
to show that `loop`{.Agda} is not `refl`{.Agda}:
```agda
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`{.Agda} which is not constantly `refl`{.Agda}.
```agda
always-loop : (x : S¹) → x ≡ x
always-loop = S¹-elim loop (double-connection loop loop)
```
## Fundamental group {defines="loop-space-of-the-circle"}
We now calculate the loop space of the circle, relative to an
_arbitrary_ implementation of the integers: any type that satisfies
their type-theoretic universal property. We call this a _HoTT take_: the
integers are the homotopy-initial space with a point and an
automorphism. What we'd like to do is prove that the loop space of the
circle is _also_ an implementation of the integers, but it's non-trivial
to show that it is a set _directly_.
```agda
module S¹Path {ℤ} (univ : Integers ℤ) where
open Integers univ
```
We start by defining a type family that we'll later find out is the
_universal cover_ of the circle. For now, it serves a humbler purpose: A
value in $\rm{Cover}(x)$ gives a concrete representation to a path
$\rm{base} \equiv x$ in the circle. We want to show that $(\rm{base}
\equiv \rm{base}) \simeq \bb{Z}$, so we set the fibre over the basepoint
to be the integers:
```agda
Cover : S¹ → Type
Cover base = ℤ
Cover (loop i) = ua rotate i
```
We can define a function from paths $\rm{base} \equiv \rm{base}$ to
integers --- or, more precisely, a function from $\rm{base} \equiv x$ to
$\rm{Cover}(x)$. Note that the path $\rm{base} \equiv x$ induces a path
$\bb{Z} \equiv \rm{Cover}(x)$, and since $\bb{Z}$ is equipped with a
choice of point, then is $\rm{Cover}(x)$.
```agda
encode : ∀ x → base ≡ x → Cover x
encode x p = subst Cover p point
```
Let us now define the inverse function: one from integer to paths. By
the mapping-out property of the integers, we must give an equivalence
from $(\rm{base} \equiv \rm{base})$ to itself. Since $(\rm{base} \equiv
\rm{base})$ is a group, any element $e$ induces such an equivalence, by
postcomposition $x \mapsto x \cdot e$. We take $e$ to be the generating
non-trivial path, $e = \rm{loop}$.
```agda
loopⁿ : ℤ → base ≡ base
loopⁿ n = map-out refl (∙-post-equiv loop) n
loopⁿ⁺¹ : (n : ℤ) → loopⁿ (rotate .fst n) ≡ loopⁿ n ∙ loop
loopⁿ⁺¹ n = map-out-rotate _ _ _
```
To prove that the map $n \mapsto \rm{loop}^n$ is an equivalence, we
shall need to extend it to a map defined fibrewise on the cover. We
shall do so cubically, i.e., by directly pattern-matching on the
argument $x$.
When we're at the base point, we already know what we want to do: we
_have_ a function $\rm{loop}^{-} : \bb{Z} \to (\rm{base} \equiv
\rm{base})$ already, so we can use that.
```agda
decode : ∀ x → Cover x → base ≡ x
decode base = loopⁿ
```
For the other case, we must
provide a path $\rm{loop}^{-} \equiv \rm{loop}^{-}$ laying over the
loop, which we can picture as the boundary of a square. Namely,
~~~{.quiver}
\[\begin{tikzcd}
{\rm{base}} && {\rm{base}} \\
\\
{\rm{base}} && {\rm{base}}
\arrow["{\rm{loop}^n}", from=1-3, to=3-3]
\arrow["{\rm{loop}}"', from=3-1, to=3-3]
\arrow["{\refl}", from=1-1, to=1-3]
\arrow["{\rm{loop}^n}"', from=1-1, to=3-1]
\end{tikzcd}\]
~~~
While it doesn't *look* like this square commutes, note that $n$ is an inhabitant
of `ua rotate i`{.Agda}, so that its values on the endpoints of `i`{.Agda} are off
by one.
If we `unglue`{.Agda} $n$, we get an integer whose incarnation at `i = i0`{.Agda}
is $1 + n$ (adjusting for the rotation offset) while at `i = i1`{.Agda} it is just $n$.
We can provide such a square as sketching out an open _cube_ whose
missing face has the boundary above. Here's such a cube: the missing
face has a dotted boundary.
~~~{.quiver .tall-2}
\[\begin{tikzcd}
{\rm{base}} &&&& {\rm{base}} \\
& {\rm{base}} && {\rm{base}} \\
\\
& {\rm{base}} && {\rm{base}} \\
{\rm{base}} &&&& {\rm{base}}
\arrow["{\rm{refl}}", from=2-2, to=2-4]
\arrow[""{name=0, anchor=center, inner sep=0}, "{\rm{loop}^{1+n}}"', from=2-2, to=4-2]
\arrow["{\rm{refl}}"', from=4-2, to=4-4]
\arrow[""{name=1, anchor=center, inner sep=0}, "{\rm{loop}^n}", from=2-4, to=4-4]
\arrow["{\rm{refl}}"{description}, dashed, from=1-1, to=1-5]
\arrow["{\rm{loop}^n}"', dashed, from=1-1, to=5-1]
\arrow["{\rm{loop}}"{description}, dashed, from=5-1, to=5-5]
\arrow["{\rm{loop}^n}", dashed, from=1-5, to=5-5]
\arrow["{\rm{refl}}"{pos=0.2}, from=2-2, to=1-1]
\arrow["{\rm{refl}}"'{pos=0.3}, from=2-4, to=1-5]
\arrow["{\rm{loop}^{-1}}"'{pos=0.1}, from=4-2, to=5-1]
\arrow["{\rm{refl}}"{pos=0.2}, from=4-4, to=5-5]
\arrow["{\rm{loop}^{\rm{unglue}(n)}}"{marking, allow upside down}, draw=none, from=0, to=1]
\end{tikzcd}\]
~~~
```agda
decode (loop i) n j = hcomp (∂ i ∨ ∂ j) λ where
k (k = i0) → loopⁿ (unglue (∂ i) n) j
k (i = i0) → ∙→square (loopⁿ⁺¹ n) (~ k) j
k (i = i1) → loopⁿ n j
k (j = i0) → base
k (j = i1) → loop (i ∨ ~ k)
```
We understand this as a particularly annoying commutative diagram. For
example, the left face expresses the equation
$\mathrm{loop}^n \bullet \mathrm{loop} = \mathrm{loop}^{1+n}$. The proof is now
straightforward to wrap up:
```agda
encode-decode : ∀ x (p : base ≡ x) → decode x (encode x p) ≡ p
encode-decode _ = J (λ x p → decode x (encode x p) ≡ p) $
ap loopⁿ (transport-refl point) ∙ map-out-point _ _
encode-loopⁿ : (n : ℤ) → encode base (loopⁿ n) ≡ n
encode-loopⁿ n = p ∙ ℤ-η n where
p : encode base (loopⁿ n) ≡ map-out point rotate n
p = map-out-unique (encode base ∘ loopⁿ)
(ap (encode base) (map-out-point _ _) ∙ transport-refl point)
(λ x → ap (encode base) {y = loopⁿ x ∙ loop} (map-out-rotate _ _ _)
·· subst-∙ Cover (loopⁿ x) loop point
·· uaβ rotate (subst Cover (loopⁿ x) point))
n
ΩS¹≃integers : (base ≡ base) ≃ ℤ
ΩS¹≃integers = Iso→Equiv $
encode base , iso loopⁿ encode-loopⁿ (encode-decode base)
open S¹Path Int-integers public
```
It immediately follows from this that the circle is a [[groupoid]], since its
loop space is a set.
```agda
opaque
S¹-is-groupoid : is-groupoid S¹
S¹-is-groupoid = S¹-elim (S¹-elim
(is-hlevel≃ 2 ΩS¹≃integers (hlevel 2)) prop!) prop!
```
<!--
```agda
instance
H-Level-S¹ : ∀ {k} → H-Level S¹ (3 + k)
H-Level-S¹ = basic-instance 3 S¹-is-groupoid
```
-->
By induction, we can show that this equivalence respects group composition
(that is, $\rm{loop}^{a + b} \equiv \rm{loop}^a \bullet \rm{loop}^b$), so that we have a
proper isomorphism of groups.
```agda
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 Groups-equational
(total-hom (Equiv.from ΩS¹≃integers ∘ Lift.lower)
(record { pres-⋆ = λ (lift a) (lift b) → loopⁿ-+ a b }))
(∙-is-equiv (Lift-≃ .snd) ((ΩS¹≃integers 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.
```agda
Ωⁿ⁺²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 Groups-equational
(Zero-group-is-terminal _ .centre)
(is-contr→≃ (is-contr→∥-∥₀-is-contr (Ωⁿ⁺²S¹-is-contr n)) (hlevel 0) .snd)
```