From: Anders Mörtberg Date: Thu, 7 Jul 2016 11:43:02 +0000 (+0200) Subject: move context of indSusp to susp X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=49a61382cdc4d0664c06846a4a35b1b799f1b1b9;p=cubicaltt.git move context of indSusp to susp --- diff --git a/examples/indSusp.ctt b/examples/indSusp.ctt deleted file mode 100644 index 4d88d12..0000000 --- a/examples/indSusp.ctt +++ /dev/null @@ -1,27 +0,0 @@ -module indSusp where - -import susp - -suspOf (A X : U) : U = (u:X) * (v:X) * (A -> Id 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 - -test1 (A X:U) (z:suspOf A X) : Id (suspOf A X) (funToL A X (lToFun A X z)) z - = refl (suspOf A X) z - -rem (A X:U) (f:susp A ->X) : (u:susp A) -> Id 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)) - -test2 (A X:U) (f:susp A ->X) : Id (susp A ->X) (lToFun A X (funToL A X f)) f - = \ (u:susp A) -> rem A X f u @ i - -funSusp (A X:U) : Id U (susp A -> X) (suspOf A X) = - isoId (susp A -> X) (suspOf A X) (funToL A X) (lToFun A X) (test1 A X) (test2 A X) diff --git a/examples/susp.ctt b/examples/susp.ctt index aa4e587..b6050d8 100644 --- a/examples/susp.ctt +++ b/examples/susp.ctt @@ -114,3 +114,29 @@ loop2S : Id sone north north = compId sone north north north loop1S loop1S -- test4S : Z = windingS (compId sone north north north loop2S loop2S) +-- indSusp: + + +suspOf (A X : U) : U = (u:X) * (v:X) * (A -> Id 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 + +test1 (A X:U) (z:suspOf A X) : Id (suspOf A X) (funToL A X (lToFun A X z)) z + = refl (suspOf A X) z + +rem (A X:U) (f:susp A ->X) : (u:susp A) -> Id 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)) + +test2 (A X:U) (f:susp A ->X) : Id (susp A ->X) (lToFun A X (funToL A X f)) f + = \ (u:susp A) -> rem A X f u @ i + +funSusp (A X:U) : Id U (susp A -> X) (suspOf A X) = + isoId (susp A -> X) (suspOf A X) (funToL A X) (lToFun A X) (test1 A X) (test2 A X)