module suspension where import proto import iso import s1 import pointed data susp (A : U) = north | south| merid (a : A) [ (i=0) -> north , (i=1) -> south ] suspension (A: U): nat -> U = split { zero -> A ; succ x -> susp (suspension A x) } Sn: nat -> U = suspension bool sn: nat -> U = split { zero -> bool ; succ x -> susp (Sn x) } S2 : U = susp S1 S3 : U = susp S2 S4 : U = susp S3 merid1 (A : U) (a : A) : Path (susp A) north south = merid {susp A} a @ i susppt (A : U) : pointed = (susp A,north) S1pt : pointed = (S1,base) S2pt : pointed = susppt S1 S3pt : pointed = susppt S2 suspS1 : susp bool -> S1 = split north -> base south -> base merid b @ i -> let case : bool -> Path S1 base base = split false -> loop1 true -> <_> base in case b @ i S1susp : S1 -> susp bool = split base -> north loop @ i -> composition (susp bool) north south north (merid1 bool false) ( merid1 bool true @ -i) @ i suspOf (A X : U) : U = (u:X) * (v:X) * (A -> Path X u v) funToL (A X:U) (f:susp A -> X) : suspOf A X = (f north,f south,\ (a:A) -> f (merid{susp A} a@i)) lToFun (A X:U) (z:suspOf A X) : susp A -> X = split north -> z.1 south -> z.2.1 merid a @ i-> z.2.2 a @ i suspOfLem (A X:U) (f:susp A ->X) : (u:susp A) -> Path X (lToFun A X (funToL A X f) u) (f u) = split north -> refl X (f north) south -> refl X (f south) merid a @ i -> refl X (f (merid{susp A} a @ i)) test1 (A X:U) (z:suspOf A X) : Path (suspOf A X) (funToL A X (lToFun A X z)) z = refl (suspOf A X) z test2 (A X:U) (f:susp A ->X) : Path (susp A ->X) (lToFun A X (funToL A X f)) f = \ (u:susp A) -> suspOfLem A X f u @ i funSusp (A X:U) : Path U (susp A -> X) (suspOf A X) = isoPath (susp A -> X) (suspOf A X) (funToL A X) (lToFun A X) (test1 A X) (test2 A X)