module Homotopy.Space.Circle.Base where
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
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)