module turn where

import helix

transpL : (A:U)(a b:A) -> Id A a b -> Id A a a -> Id A b b
transpL A a b p l = (compInv A a b b p (comp A a a b l p))

lemTranspL : (A:U)(a:A)(l:Id A a a) -> Id (Id A a a) l (transpL A a a (refl A a) l)
lemTranspL A a l = rem2
 where
  l1 : Id A a a
  l1 = comp A a a a l (refl A a)
  rem : Id (Id A a a) l1 l
  rem = compIdr A a a l
  rem1 : Id (Id A a a) l1 (compInv A a a a (refl A a) l1) 
  rem1 = compInvIdl' A a a l1
  rem2 : Id (Id A a a) l (compInv A a a a (refl A a) l1) 
  rem2 = compInv (Id A a a) l1 l (compInv A a a a (refl A a) l1) rem rem1

lemTranspL1 : (A:U)(a:A)(l:Id A a a) -> Id (Id A a a) l (transpL A a a l l)
lemTranspL1 A a l = lemInv A a a a l l

lemG0 : (A:U)(a b:A)(p:Id A a b)(l : Id A a a) -> 
        IdS A (\ x -> Id A x x) a b p l (transpL A a b p l)
lemG0 A a = J A a (\ b p -> (l : Id A a a) -> IdS A (\ x -> Id A x x) a b p l (transpL A a b p l))
              (lemTranspL A a)

lemG1 : (A:U)(a:A)(l:Id A a a) -> IdS A (\ x -> Id A x x) a a l l l
lemG1 A a l = 
 substInv (Id A a a) (IdS A (\ x -> Id A x x) a a l l) l (transpL A a a l l) 
    (lemTranspL1 A a l) (lemG0 A a a l l)

lp : (x:S1) -> Id S1 x x
lp = S1rec (\ x -> Id S1 x x) loop (lemG1 S1 base loop)

lp1 : S1 -> S1
lp1 x = S1rec (\ _ -> S1) x (lp x) x

path : Id S1 base base
path = mapOnPath S1 S1 lp1 base base loop

test : Z
test = winding path

path2 : Id S1 base base
path2 = mapOnPath S1 S1 lp1 base base (compS1 loop (compS1 loop loop))

test2 : Z
test2 = winding path2