{- HIT:
   - 1-Sphere HIT.
   Copyright (c) Groupoid Infinity, 2014-2018.

   HoTT 6.4 Circles and spheres -}

module s1 where
import int

data S1 = base
        | loop <i> [ (i=0) -> base ,
                     (i=1) -> base ]

loopS1 : U = Path S1 base base
compS1 : loopS1 -> loopS1 -> loopS1 = composition S1 base base base

-- All of these should be equal to "posZ (suc zero)":
loop1 : loopS1 = <i> loop{S1} @ i
loop2 : loopS1 = compS1 loop1 loop1
loop3 : loopS1 = composition S1 base base base loop1 loop1
loop4 : loopS1 = compS1 loop2 loop1

triv      : loopS1 = <i> base
invLoop   : loopS1 = inv S1 base base loop1
oneTurn   : loopS1 -> loopS1 = \(l: loopS1) -> compS1 l loop1
backTurn  : loopS1 -> loopS1 = \(l: loopS1) -> compS1 l invLoop
l0        : loopS1 = triv
l1        : loopS1 = oneTurn l0
loopPos   : nat -> loopS1 = split { zero -> triv ; succ n -> oneTurn (loopPos n) }
loopNeg   : nat -> loopS1 = split { zero -> invLoop ; succ n -> backTurn (loopNeg n) }
ze    (x: nat):    bool -> Z      = split { false -> inl x      ; true -> inr x }
loopZ (x: nat):    bool -> loopS1 = split { false -> loopNeg x  ; true -> loopPos x }
turnZ (x: loopS1): bool -> loopS1 = split { false -> backTurn x ; true -> oneTurn x }
inversion:         bool -> loopS1 = split { false -> <i> loop1 @ -i ; true -> loop1 }
lnb   (n: nat) (b: bool):  loopS1 = loopZ n b
loopIt    : Z   -> loopS1 = split { inl n -> loopNeg n ; inr n -> loopPos n }
compInvS1 : Path loopS1 (refl S1 base) (compS1 invLoop loop1) =
  compInv' S1 base base loop1

-- Helix for Winding
helix : S1 -> U = split { base -> Z ; loop @ i -> sucPathZ @ i }
winding (p : loopS1) : Z = trans Z Z (<i> helix (p @ i)) zeroZ
htl (n: nat) (b: bool): Path U Z Z = <i> helix (turnZ (loopZ n b) b @ i)
htl' (n: nat) (b: bool): Path U Z Z = <i> helix (loopZ n b @ i)
hlx: bool-> Path U Z Z = split { false -> <i>helix (loop1@-i) ; true -> <i>helix (loop1@i) }
htz (n: nat) (b: bool): Z = comp (htl n b) (inr zero) []

-- More examples:
loopZ1  : Z = winding loop1
loopZ2  : Z = winding (compS1 loop1 loop1)
loopZ3  : Z = winding (compS1 loop1 (compS1 loop1 loop1))
loopZN1 : Z = winding invLoop
loopZ0  : Z = winding (compS1 loop1 invLoop)

mLoop : (x : S1) -> Path S1 x x = split
  base -> loop1
  loop @ i -> (constSquare S1 base loop1) @ i

mult (x : S1) : S1 -> S1 = split
  base -> x
  loop @ i -> mLoop x @ i

square (x : S1) : S1 = mult x x
doubleLoop (l : loopS1) : loopS1 = <i> square (l @ i)
tripleLoop (l : loopS1) : loopS1 = <i> mult (l @ i) (square (l @ i))

loopZ4 : Z = winding (doubleLoop (compS1 loop1 loop1))
loopZ8 : Z = winding (doubleLoop (doubleLoop (compS1 loop1 loop1)))

-- A nice example of a homotopy on the circle. The path going halfway
-- around the circle and then back is contractible:
circ_hmtpy : Path loopS1 (<i> base) (<i> loop{S1} @ (i /\ -i)) =
  <j i> loop{S1} @ j /\ i /\ -i

circleelim (X : U) (x : X) (p : Path X x x) : S1 -> X = split
  base -> x
  loop @ i -> p @ i

apcircleelim (A B : U) (x : A) (p : Path A x x) (f : A -> B) :
  (z : S1) -> Path B (f (circleelim A x p z))
                   (circleelim B (f x) (<i> f (p @ i)) z) = split
   base -> <_> f x
   loop @ i -> <_> f (p @ i)

-- a special case, Lemmas 6.2.5-6.2.9 in the book

aLoop (A:U) : U = (a:A) * Path A a a

phi (A:U) (al : aLoop A) : S1 -> A = split
  base -> al.1
  loop @ i -> (al.2)@ i

psi (A:U) (f:S1 -> A) : aLoop A = (f base,<i>f (loop1@i))

rem (A:U) (f : S1 -> A) : (u : S1) -> Path A (phi A (psi A f) u) (f u) = split
         base -> refl A (f base)
         loop @ i -> <j>f (loop1@i)

lem (A:U) (f : S1 -> A) : Path (S1 -> A) (phi A (psi A f)) f = 
 <i> \ (x:S1) -> (rem A f x) @ i

thm (A:U) : Path U (aLoop A) (S1 -> A) = isoPath T0 T1 f g t s
 where T0 : U = aLoop A
       T1 : U = S1 -> A
       f : T0 -> T1 = phi A
       g : T1 -> T0 = psi A
       s (x:T0) : Path T0 (g (f x)) x    = refl T0 x
       t : (y:T1) -> Path T1 (f (g y)) y = lem A

lem1ItPos : (n:nat) -> Path loopS1 (loopIt (sucZ (inr n))) (oneTurn ((loopIt (inr n)))) = split
  zero -> refl loopS1 l1
  succ p -> <i>oneTurn (lem1ItPos p@i)

lem1ItNeg : (n:nat) -> Path loopS1  (loopIt (sucZ (inl n))) (oneTurn (loopIt (inl n))) = split
  zero -> compInvS1
  succ p -> compInv S1 base base (loopIt (inl p)) base invLoop

lem1It : (n:Z) -> Path loopS1 (loopIt (sucZ n)) (oneTurn  (loopIt n)) = split
  inl n -> lem1ItNeg n
  inr n -> lem1ItPos n