From: coquand Date: Wed, 29 Apr 2015 10:28:10 +0000 (+0200) Subject: added hopf fibration X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=b415b803449a44ddfef3b35e22076a321d15bc70;p=cubicaltt.git added hopf fibration --- diff --git a/examples/hopf.ctt b/examples/hopf.ctt new file mode 100644 index 0000000..b4a02f4 --- /dev/null +++ b/examples/hopf.ctt @@ -0,0 +1,10 @@ +module hopf where + +import truncS2 +import mult + +hopf : S2 -> U = split + north -> S1 + south -> S1 + merid x @ i -> eqS1 x @ i + diff --git a/examples/mult.ctt b/examples/mult.ctt index d6f0f37..a0a88cf 100644 --- a/examples/mult.ctt +++ b/examples/mult.ctt @@ -9,21 +9,24 @@ invS : S1 -> S1 = split base -> base loop @ i -> loop1 @ -i + + lemInv : (x:S1) -> Id S1 (mult x (invS x)) base = split base -> refl S1 base - loop @ i -> loop1 @i\/-i\/j + loop @ i -> base test0S : Z = winding (mult (loop2@i) (invS (loop2@i))) +loop4 : loopS1 = compS1 loop2 loop2 test00S : Z = winding (mult (loop4@i) (invS (loop4@i))) lemInv1 : (x:S1) -> Id S1 (mult (invS x) x) base = split base -> refl S1 base - loop @ i -> loop1 @ -i\/i\/j + loop @ i -> base -- loop1 @ -i\/i\/j test : loopS1 = mult (loop1@i) (loop1@-i) test1 : IdP (Id S1 (mult (loop1@i) base) (mult (loop1@i) base)) loop1 loop1 = mult (loop1@i) (loop1@j) test2 : loopS1 = mult (loop1@i) (loop1@i) -test3 : Id loopS1 test2 (compS1 loop1 loop1) = refl loopS1 test2 +-- test3 : Id loopS1 test2 (compS1 loop1 loop1) = refl loopS1 test2 lemBase (y:S1) : Id S1 (mult base (mult base y)) y = compId S1 (mult base (mult base y)) (mult base y) y (idL (mult base y)) (idL y)