From: Anders Mörtberg Date: Mon, 20 Apr 2015 08:12:57 +0000 (+0200) Subject: Fix all the old examples of HITs X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=d5d7b5f88af921768e85e79d2df3beda987ddcc5;p=cubicaltt.git Fix all the old examples of HITs --- diff --git a/examples/circle.ctt b/examples/circle.ctt index 758e412..44da52b 100644 --- a/examples/circle.ctt +++ b/examples/circle.ctt @@ -4,7 +4,7 @@ import bool import int data S1 = base - | loop @ base ~ base + | loop [(i=0) -> base, (i=1) -> base] loopS1 : U = Id S1 base base diff --git a/examples/higherhit.ctt b/examples/higherhit.ctt index e6993bd..4b6b085 100644 --- a/examples/higherhit.ctt +++ b/examples/higherhit.ctt @@ -7,7 +7,7 @@ import prelude -- old stuff looks now like this data S1 = base - | loop @ [(i=0) -> base, (i=1) -> base] + | loop [(i=0) -> base, (i=1) -> base] foo : S1 = base @@ -18,25 +18,25 @@ loop' : Id S1 base base = (loop {S1}) @ i -- new data S2 = base - | loop2 @ [ (i=0) -> base - , (i=1) -> base - , (j=0) -> base - , (j=1) -> base] + | loop2 [ (i=0) -> base + , (i=1) -> base + , (j=0) -> base + , (j=1) -> base] loop2' : Id (Id S2 base base) (refl S2 base) (refl S2 base) = loop2 {S2} @ i @ j data Torus = ptT - | pathOneT @ [ (i=0) -> ptT, (i=1) -> ptT ] - | pathTwoT @ [ (i=0) -> ptT, (i=1) -> ptT ] - | squareT @ [ (i=0) -> pathOneT {Torus} @ j - , (i=1) -> pathOneT {Torus} @ j - , (j=0) -> pathTwoT {Torus} @ i - , (j=1) -> pathTwoT {Torus} @ i ] + | pathOneT [ (i=0) -> ptT, (i=1) -> ptT ] + | pathTwoT [ (i=0) -> ptT, (i=1) -> ptT ] + | squareT [ (i=0) -> pathOneT {Torus} @ j + , (i=1) -> pathOneT {Torus} @ j + , (j=0) -> pathTwoT {Torus} @ i + , (j=1) -> pathTwoT {Torus} @ i ] data setTrunc (A : U) = inc (a : A) - | setTr (a b : setTrunc A) (p q : Id (setTrunc A) a b) @ + | setTr (a b : setTrunc A) (p q : Id (setTrunc A) a b) [ (i=0) -> p @ j , (i=1) -> q @ j , (j=0) -> a diff --git a/examples/integer.ctt b/examples/integer.ctt index e3d4d8b..57c5db2 100644 --- a/examples/integer.ctt +++ b/examples/integer.ctt @@ -4,7 +4,7 @@ import int data int = pos (n : nat) | neg (n : nat) - | zeroP @ pos zero ~ neg zero + | zeroP [(i=0) -> pos zero, (i=1) -> neg zero] zeroP' : Id int (pos zero) (neg zero) = zeroP {int} @ i diff --git a/examples/interval.ctt b/examples/interval.ctt index d5a2c43..ca455da 100644 --- a/examples/interval.ctt +++ b/examples/interval.ctt @@ -2,7 +2,7 @@ module interval where import prelude -data I = zero | one | seg @ zero ~ one +data I = zero | one | seg [(i = 0) -> zero, (i = 1) -> one] -- Proof of funext from the interval fext (A B : U) (f g : A -> B) (p : (x : A) -> Id B (f x) (g x)) : diff --git a/examples/susp.ctt b/examples/susp.ctt index ef53a7a..1224b14 100644 --- a/examples/susp.ctt +++ b/examples/susp.ctt @@ -4,7 +4,7 @@ import circle data susp (A : U) = north | south - | merid (a:A) @ north ~ south + | merid (a:A) [(i=0) -> north, (i=1) -> south] -- n-spheres sphere : nat -> U = split