From: Anders Date: Mon, 20 Apr 2015 14:10:57 +0000 (+0200) Subject: Split higherhit into multiple files X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=53695768f7595192b5795170f94c30319c778bdc;p=cubicaltt.git Split higherhit into multiple files --- diff --git a/examples/higherhit.ctt b/examples/higherhit.ctt deleted file mode 100644 index 4a501a5..0000000 --- a/examples/higherhit.ctt +++ /dev/null @@ -1,60 +0,0 @@ -module higherhit where - -import prelude - --- Some experiments with higher HITs. - --- old stuff looks now like this - -data S1 = base - | loop [(i=0) -> base, (i=1) -> base] - - -foo : S1 = base - -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' : 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 ] - -data setTrunc (A : U) - = inc (a : A) - | setTr (a b : setTrunc A) (p q : Id (setTrunc A) a b) - [ (i=0) -> p @ j - , (i=1) -> q @ j - , (j=0) -> a - , (j=1) -> b] - -setTruncSet (A : U) : set (setTrunc A) = - \(a b : setTrunc A) (p q : Id (setTrunc A) a b) -> - setTr {setTrunc A} a b p q @ i @ j - - -setTruncRec (A : U) - (B : U) - (bS : set B) - (f : A -> B) : - setTrunc A -> B = - split - inc a -> f a - setTr a b p q @ i j -> (bS (setTruncRec A B bS f a) - (setTruncRec A B bS f b) - ( setTruncRec A B bS f (p @ k)) - ( setTruncRec A B bS f (q @ k))) @ i @ j diff --git a/examples/s2.ctt b/examples/s2.ctt new file mode 100644 index 0000000..359ddf9 --- /dev/null +++ b/examples/s2.ctt @@ -0,0 +1,12 @@ +module s2 where + +import prelude + +data S2 = 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 diff --git a/examples/setTrunc.ctt b/examples/setTrunc.ctt new file mode 100644 index 0000000..bd34fba --- /dev/null +++ b/examples/setTrunc.ctt @@ -0,0 +1,28 @@ +module setTrunc where + +import prelude + +data setTrunc (A : U) + = inc (a : A) + | setTr (a b : setTrunc A) (p q : Id (setTrunc A) a b) + [ (i=0) -> p @ j + , (i=1) -> q @ j + , (j=0) -> a + , (j=1) -> b] + +setTruncSet (A : U) : set (setTrunc A) = + \(a b : setTrunc A) (p q : Id (setTrunc A) a b) -> + setTr {setTrunc A} a b p q @ i @ j + + +setTruncRec (A : U) + (B : U) + (bS : set B) + (f : A -> B) : + setTrunc A -> B = + split + inc a -> f a + setTr a b p q @ i j -> (bS (setTruncRec A B bS f a) + (setTruncRec A B bS f b) + ( setTruncRec A B bS f (p @ k)) + ( setTruncRec A B bS f (q @ k))) @ i @ j diff --git a/examples/torus.ctt b/examples/torus.ctt new file mode 100644 index 0000000..1300a27 --- /dev/null +++ b/examples/torus.ctt @@ -0,0 +1,11 @@ +module torus where + +import prelude + +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 ]