open import 1Lab.Path.Groupoid open import 1Lab.Univalence open import 1Lab.Type.Dec open import 1Lab.Equiv open import 1Lab.Path open import 1Lab.Type open import Data.Int.Inductive open import Data.Bool open import Data.Bool module 1Lab.HIT.S1 where

# The Circle🔗

Since the “intended interpretation” of HoTT is in a $\io$-category of “good spaces”, it makes sense that HoTT has facilities for describing spaces. These are the *higher inductive types*, one of which is the **circle**:

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

Using möbius, it can be shown that the 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. By S¹-elim', we can prove that there is an inhabitant of `(x : S¹) → x ≡ x`

which is not constantly refl

S¹-elim : ∀ {ℓ} {P : S¹ → Type ℓ} → (pb : P base) → PathP (λ i → P (loop i)) pb pb → (x : S¹) → P x S¹-elim pb pl base = pb S¹-elim pb pl (loop i) = pl i S¹-elim' : ∀ {ℓ} {P : S¹ → Type ℓ} (pb : P base) → subst P loop pb ≡ pb → (x : S¹) → P x S¹-elim' {P = P} pb pl = S¹-elim pb (transport (λ i → PathP≡Path (λ i → P (loop i)) pb pb (~ i)) pl) always-loop : (x : S¹) → x ≡ x always-loop = S¹-elim' loop (subst-path-both _ _ ∙ lemma) where lemma = sym loop ∙ loop ∙ loop ≡⟨ ∙-cancel-l loop loop ⟩≡ loop ∎

## Path Space🔗

A classical result of algebraic topology is that the fundamental group of the circle is isomorphic to the group of integers. In Homotopy Type Theory, we can repeat this proof: The type of integers *codes for* paths in the circle.

module S¹Path where Cover : S¹ → Type Cover base = Int Cover (loop i) = ua suc-equiv i

We define a map encode which converts a path in the circle to an element of the Cover. By lifting p to the Cover, we determine a path `Int ≡ Int`

, which we apply to zero:

encode : (x : S¹) → base ≡ x → Cover x encode x p = subst Cover p (pos zero)

This map counts the *winding number* of a path:

_ : encode base refl ≡ pos zero _ = refl _ : encode base loop ≡ pos (suc zero) _ = refl

In the other direction, we define a map decode which converts an integer to a path `base ≡ base`

:

loop^ : Int → base ≡ base loop^ (pos zero) = refl loop^ (pos (suc x)) = loop^ (pos x) ∙ loop loop^ (negsuc zero) = sym loop loop^ (negsuc (suc x)) = loop^ (negsuc x) ∙ sym loop

What we want to show is that `encode base`

and `loop^`

are mutual inverses. For this, we must show that `encode base (loop^ n) ≡ n`

and `loop^ (encode base p) ≡ p`

. The former direction is simpler, because we can show it directly by recursion on Int:

encode-loop^ : (n : Int) → encode base (loop^ n) ≡ n encode-loop^ (pos zero) = refl encode-loop^ (pos (suc x)) = ap suc-int (encode-loop^ (pos x)) encode-loop^ (negsuc zero) = refl encode-loop^ (negsuc (suc x)) = ap pred-int (encode-loop^ (negsuc x))

In the other direction, we would like to apply *path induction* to reduce the problem to showing `loop^ (encode base refl) ≡ refl`

. However, path induction does not apply to paths `base ≡ base`

, only to paths `base ≡ x`

, where `x`

a variable. Therefore, we have to generalise the function `loop^`

to the function decode.

decode : (x : S¹) → Cover x → base ≡ x decode base = loop^

On the basepoint, the type of the right-hand side computes to `Int → base ≡ base`

; Thus, we can use the existing loop^ map.

decode (loop i) n j = square where

For the loop case, recall the induction principle of the circle. We must provide a path `loop^ ≡ loop^`

“laying over” loop, i.e. a `Square refl (loop^ n) (loop^ n) loop`

. Visually, we can picture the boundary of the path we must provide as the square below:

We will construct this square in parts. First, we’ll construct a square loop^-square with the boundary below, for any $n$, by recursion on the integer $n$; We’ll then modify this square so it becomes the one above.

loop^-square : (n : Int) → Square refl (loop^ (pred-int n)) (loop^ n) loop loop^-square (pos zero) i j = loop (i ∨ ~ j)

The case above is for $n = 0$. We can picture it as follows. Note that this is a square where two faces are the path loop and two faces are degenerate: a connection.

loop^-square (pos (suc x)) i j = hfill (λ k → λ { (j = i0) → base ; (j = i1) → loop k }) (inS (loop^ (pos x) j)) i

In the case where $n = +x$, the square we have to fill is the one on the left below, but note that the composite on the right face is *defined* to be the dashed path in that square; Thus, the filler of that square suffices. A similar thing happens for the case where $n = -(x + 1)$, which is the square on the right.

loop^-square (negsuc x) i j = hfill (λ k → λ { (j = i0) → base ; (j = i1) → loop (~ k) }) (inS (loop^ (negsuc x) j)) (~ i)

We can then alter the square loop^-square to the square we want, by sketching an appropriate cube.

square = hcomp (λ k → λ { (i = i0) → loop^ (pred-suc n k) j ; (i = i1) → loop^ n j ; (j = i0) → base ; (j = i1) → loop i }) (loop^-square (unglue (i ∨ ~ i) n) i j)

With this generalised decode, we can prove that `decode x (encode x p) ≡ p`

, by reducing `p`

to refl, i.e. path induction.

decode-encode : {x : S¹} (p : base ≡ x) → decode x (encode x p) ≡ p decode-encode = J (λ y p → decode y (encode y p) ≡ p) refl

Thus we have that the loop space of the circle is the type of integers:

ΩS¹≃Int : (base ≡ base) ≃ Int ΩS¹≃Int = Iso→Equiv (encode base , iso loop^ encode-loop^ decode-encode)