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)