cubical-0.2.0: examples/helix.cub

module helix where

import integer

helix : S1 -> U
helix = S1rec (\_ -> U) Z sucIdZ

test : Id U Z (helix base)
test = refl U Z

loopSpace : (A : U) (a : A) -> U
loopSpace A a = Id A a a

loopS1 : U
loopS1 = loopSpace S1 base

S1recbase : (F : S1 -> U) (b : F base) -> (l : IdS S1 F base base loop b b) ->
  Id (F base) (S1rec F b l base) b
S1recbase F b l = refl (F base) b

-- S1recloop : (F : S1 -> U) (b : F base) -> (l : IdS S1 F base base loop b b) ->
--  Id (IdS S1 F base base loop b b)
--    (mapOnPathD S1 F (S1rec F b l) base base loop)
--    l
-- S1recloop F b l = refl (IdS S1 F base base loop b b) l

winding : loopS1 -> Z
winding l = transport Z Z (rem l) zeroZ
  where
    rem : loopS1 -> Id U Z Z
    rem l = mapOnPath S1 U helix base base l

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

invS1 : loopS1 -> loopS1
invS1 = inv S1 base base

test1 : Z
test1 = winding loop

loop2 : loopS1
loop2 = compS1 loop loop

loop4 : loopS1
loop4 = compS1 loop2 loop2

loop8 : loopS1
loop8 = compS1 loop4 loop4

test2 : Z
test2 = winding (compS1 loop (invS1 loop))

test3 : Z
test3 = winding (invS1 loop2)

test4 : Z
test4 = winding (compS1 loop4 (invS1 loop2))

test5 : Z
test5 = winding (compS1 loop8 (invS1 loop2))

encode : (x : S1) -> Id S1 base x -> helix x
encode x l = subst S1 helix base x l zeroZ

loopN : N -> loopS1
loopN = split
  zero -> refl S1 base
  suc n -> compS1 loop (loopN n)

loopZ : Z -> loopS1
loopZ = split
  inl n -> invS1 (loopN (suc n))
  inr n -> loopN n

-- loopZpred : (n : Z) -> Id loopS1 (loopZ (predZ n)) (compS1 (invS1 loop) (loopZ n))
-- loopZpred n = undefined

testDan : Id U Z Z 
testDan = mapOnPath S1 U helix base base loop

funDan : Z -> Z
funDan = transport Z Z testDan

funDan1 : Z -> Z
funDan1 = transport Z Z sucIdZ

-- testDan1 : Id (Z->Z) sucZ funDan1
-- testDan1 = refl (Z -> Z) sucZ

test0 : Z
test0 = transport Z Z testDan zeroZ

vect : N -> U
vect = split 
         zero -> Unit
         suc n -> and N (vect n)

Peter : S1 -> N
Peter = S1rec (\ _ -> N) zero (refl N zero)

testPeter : Id N zero zero
testPeter = mapOnPath S1 N Peter base base loop


-- helix = S1rec (\_ -> U) Z sucIdZ