circle.ctt

-- The circle as a HIT.
module circle where

import bool
import int

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

loopS1 : U = Path S1 base base

loop1 : loopS1 = <i> loop{S1} @ i

invLoop : loopS1 = inv S1 base base loop1

moebius : S1 -> U = split
  base -> bool
  loop @ i -> negBoolEq @ i

helix : S1 -> U = split
  base -> Z
  loop @ i -> sucPathZ @ i

winding (p : loopS1) : Z = trans Z Z rem zeroZ
  where
    rem : Path U Z Z = <i> helix (p @ i)

compS1 : loopS1 -> loopS1 -> loopS1 = compPath S1 base base base

-- All of these should be equal to "posZ (suc zero)":
loop2 : loopS1 = compS1 loop1 loop1
loop2' : loopS1 = compPath' S1 base base base loop1 loop1
loop2'' : loopS1 = compPath'' S1 base base loop1 base loop1

-- 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)
loopZ5  : Z = winding (compS1 loop1 (compS1 loop1 (compS1 loop1 (compS1 loop1 loop1))))

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)))

triv : loopS1 = <i> base

-- A nice example of a homotopy on the circle. The path going halfway
-- around the circle and then back is contractible:
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