From: coquand Date: Tue, 28 Apr 2015 16:33:36 +0000 (+0200) Subject: an example of normal form X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=42434ef8cb9aa3790a6c043b6e3ab0943ff08b06;p=cubicaltt.git an example of normal form --- diff --git a/examples/pi1S2.ctt b/examples/pi1S2.ctt index 0171f22..9515108 100644 --- a/examples/pi1S2.ctt +++ b/examples/pi1S2.ctt @@ -1,6 +1,7 @@ module pi1S2 where import truncS2 +import susp import groupoidTrunc lemGrp4 (X : U) (gX:groupoid X) : Id U (gTrunc S2 -> X) X @@ -21,5 +22,31 @@ corr2 (x:gTrunc S2) : Id (gTrunc S2) x (inc north) = corr1@i x test : Id (gTrunc S2) (inc south) (inc north) = corr2 (inc south) +-- normal form + +test : Id (gTrunc S2) (inc south) (inc north) = + inc (comp S2 north + [ (i = 0) -> comp S2 south + [ (j = 0) -> comp S2 north + [ (k = 0) -> comp S2 south + [ (l = 0) -> comp S2 north + [ (m = 0) -> comp S2 south + [ (n = 0) ->

comp S2 north + [ (p = 0) -> comp S2 north [ (q = 1) -> merid {S2} base @ r ] ] ] ] ] ] ] ]) + + + test1 : Id (gTrunc S2) (inc north) (inc north) = corr2 (inc north) +-- this should imply that any element in gTrunc (susp sone) is equal to inc north + + + +stwo : U = susp sone + +corr3 : (x:gTrunc stwo) -> Id (gTrunc stwo) x (inc north) = + transport ((x:gTrunc (susp (s1EqCircle@-i))) -> Id (gTrunc (susp (s1EqCircle@-i))) x (inc north)) corr2 + +test2 : Id (gTrunc stwo) (inc south) (inc north) = corr3 (inc south) + +-- corr2 (x:gTrunc S2) : Id (gTrunc S2) x (inc north) = corr1@i x \ No newline at end of file