open import 1Lab.Prelude

open import Data.Bool

open import Homotopy.Loopspace

module Homotopy.Space.Circle.Base where

private variable
  ℓ ℓ' : Level
  X : Type ℓ

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)