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

Diagramatically, we can picture the circle as being the $\infty$-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 two different paths:

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:

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)

## Fundamental group🔗

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

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
$\mathrm{Cover}(x)$
gives a concrete representation to a path
$\mathrm{base} \equiv x$
in the circle. We want to show that
$(\mathrm{base} \equiv \mathrm{base}) \simeq \mathbb{Z}$,
so we set the fibre over the basepoint to be the integers:

Cover : S¹ → Type Cover base = ℤ Cover (loop i) = ua rotate i

We can define a function from paths $\mathrm{base} \equiv \mathrm{base}$ to integers — or, more precisely, a function from $\mathrm{base} \equiv x$ to $\mathrm{Cover}(x)$. Note that the path $\mathrm{base} \equiv x$ induces a path $\mathbb{Z} \equiv \mathrm{Cover}(x)$, and since $\mathbb{Z}$ is equipped with a choice of point, then is $\mathrm{Cover}(x)$.

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 $(\mathrm{base} \equiv \mathrm{base})$ to itself. Since $(\mathrm{base} \equiv \mathrm{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 = \mathrm{loop}$.

post-loop : (base ≡ base) ≃ (base ≡ base) post-loop = Iso→Equiv $ (_∙ loop) , iso (_∙ sym loop) (λ p → sym (∙-assoc p _ _) ·· ap (p ∙_) (∙-invl loop) ·· ∙-idr p) (λ p → sym (∙-assoc p _ _) ·· ap (p ∙_) (∙-invr loop) ·· ∙-idr p) loopⁿ : ℤ → base ≡ base loopⁿ n = map-out refl post-loop n

To prove that the map $n \mapsto \mathrm{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$.

square-loopⁿ : (n : ℤ) → Square refl (loopⁿ (Equiv.from rotate n)) (loopⁿ n) loop square-loopⁿ n = commutes→square $ sym $ ⌜ loopⁿ (Equiv.from rotate n) ⌝ ∙ loop ≡⟨ ap! (map-out-rotate-inv _ _ _) ⟩≡ (loopⁿ n ∙ sym loop) ∙ loop ≡⟨ ∙-cancelr _ _ ⟩≡ loopⁿ n ≡⟨ sym (∙-idl _) ⟩≡ refl ∙ loopⁿ n ∎

When we’re at the base point, we already know what we want to do: we
*have* a function
$\mathrm{loop}^{-} : \mathbb{Z} \to (\mathrm{base} \equiv \mathrm{base})$
already, so we can use that. For the other case, we must provide a path
$\mathrm{loop}^{-} \equiv \mathrm{loop}^{-}$
laying over the loop, which we can picture as the boundary of a square.
Namely,

decode : ∀ x → Cover x → base ≡ x decode base = loopⁿ

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.

decode (loop i) code j = hcomp (∂ i ∨ ∂ j) λ where k (k = i0) → square-loopⁿ (unglue (∂ i) code) i j k (i = i0) → loopⁿ (Equiv.η rotate code k) j k (i = i1) → loopⁿ code j k (j = i0) → base k (j = i1) → loop i

We understand this as a particularly annoying commutative diagram. For example, the front face expresses the equation $\mathrm{loop}^{n-1}\mathrm{loop} = \mathrm{loop}^{n}$. The proof is now straightforward to wrap up:

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 ∙ sym (map-out-unique id refl (λ _ → refl) 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