index ∙ source

open import 1Lab.Prelude
open import 1Lab.Reflection.Induction

open import Data.Bool

open import Homotopy.Space.Circle

module DoubleCoverOfTheCircle where

double cover of the circle

We define the connected double cover of the circle in two ways, as a higher inductive family and by recursion, and show that the two definitions are equivalent.

The higher inductive definition has two $n$-cells for every $n$-cell in the circle: two points over $\mathsf{base}$ and two loops over $\mathsf{loop}$.

data Cover : S¹ → Type where
  base0 base1 : Cover base
  loop0 : PathP (λ i → Cover (loop i)) base0 base1
  loop1 : PathP (λ i → Cover (loop i)) base1 base0

unquoteDecl Cover-elim =
  make-elim-with default-elim-visible Cover-elim (quote Cover)

The recursive definition defines a $2$-element set bundle directly by sending $\mathsf{base}$ to the booleans and $\mathsf{loop}$ to the identification that swaps the booleans, using univalence.

cover : S¹ → Type
cover = S¹-elim Bool (ua not≃)

We can then write functions in both directions and prove that they are inverses using the introduction and elimination helpers for ua.

recover : ∀ s → Cover s → cover s
recover = Cover-elim _ true false
  (path→ua-pathp _ refl) (path→ua-pathp _ refl)

discover-base : cover base → Cover base
discover-base true = base0
discover-base false = base1

discover-loop
  : ∀ c → PathP (λ i → Cover (loop i)) (discover-base c) (discover-base (not c))
discover-loop true = loop0
discover-loop false = loop1

discover : ∀ s → cover s → Cover s
discover = S¹-elim discover-base (ua→ discover-loop)

rediscover : ∀ s c → recover s (discover s c) ≡ c
rediscover = S¹-elim (Bool-elim _ refl refl) hlevel!

disrecover : ∀ s c → discover s (recover s c) ≡ c
disrecover = Cover-elim _ refl refl
  (transposeP (ua→-β not≃ {f₁ = discover-base} discover-loop refl ∙ ▷-idr loop0))
  (transposeP (ua→-β not≃ {f₁ = discover-base} discover-loop refl ∙ ▷-idr loop1))

Cover≃cover : ∀ s → Cover s ≃ cover s
Cover≃cover s = recover s , is-iso→is-equiv λ where
  .is-iso.from → discover s
  .is-iso.rinv → rediscover s
  .is-iso.linv → disrecover s