From: Anders <mortberg@chalmers.se>
Date: Thu, 26 Mar 2015 15:52:46 +0000 (+0100)
Subject: Add the circle (there is a bug)
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=ecce1c71e9185d7b94e39adfc9838f9c9a808318;p=cubicaltt.git

Add the circle (there is a bug)
---

diff --git a/examples/circle.ctt b/examples/circle.ctt
new file mode 100644
index 0000000..6e68af3
--- /dev/null
+++ b/examples/circle.ctt
@@ -0,0 +1,26 @@
+module circle where
+
+import bool
+import integer
+
+data S1 = base | loop @ base ~ base
+
+moebius : S1 -> U = split
+  base -> bool
+  loop @ i -> negEq @ i
+
+loop' : Id S1 base base = <i> loop{S1} @ i
+
+helix : S1 -> U = split
+  base -> Z
+  loop @ i -> sucIdZ @ i
+
+loopS1 : U = Id S1 base base 
+
+winding (p : loopS1) : Z = transport rem zeroZ
+  where
+    rem : Id U Z Z = <i> helix (p @ i)
+
+loop2 : loopS1 = compId S1 base base base loop' loop'
+loop2' : loopS1 = compId' S1 base base base loop' loop'
+loop2'' : loopS1 = compId'' S1 base base loop' base loop'
\ No newline at end of file
diff --git a/examples/integer.ctt b/examples/integer.ctt
new file mode 100644
index 0000000..2f08c7b
--- /dev/null
+++ b/examples/integer.ctt
@@ -0,0 +1,39 @@
+module integer where
+
+import nat
+
+data Z = zeroZ | posZ (n : nat) | negZ (n : nat)
+
+caseNat (A : U) (a : A) (f : nat -> A) : nat -> A = split
+  zero -> a
+  suc n -> f n
+
+sucZ : Z -> Z = split
+  zeroZ -> posZ zero
+  posZ n -> posZ (suc n)
+  negZ n -> caseNat Z zeroZ (\(x : nat) -> negZ x) n
+
+predZ : Z -> Z = split
+  zeroZ -> negZ zero
+  posZ n -> caseNat Z zeroZ (\(x : nat) -> posZ x) n
+  negZ n -> negZ (suc n)
+
+sucpredZ : (n : Z) -> Id Z (sucZ (predZ n)) n = split
+  zeroZ  -> refl Z zeroZ
+  posZ n -> lem n
+   where
+    lem : (n : nat) -> Id Z (sucZ (predZ (posZ n))) (posZ n) = split
+      zero  -> refl Z (posZ zero)
+      suc n -> refl Z (posZ (suc n))
+  negZ n -> refl Z (negZ n)
+
+predsucZ : (n : Z) -> Id Z (predZ (sucZ n)) n = split
+  zeroZ -> refl Z zeroZ
+  posZ n -> refl Z (posZ n)
+  negZ n -> lem n
+   where
+    lem : (n : nat) -> Id Z (predZ (sucZ (negZ n))) (negZ n) = split
+      zero  -> refl Z (negZ zero)
+      suc n -> refl Z (negZ (suc n))
+
+sucIdZ : Id U Z Z = isoId Z Z sucZ predZ sucpredZ predsucZ
diff --git a/examples/prelude.ctt b/examples/prelude.ctt
index 51c1594..4abdb03 100644
--- a/examples/prelude.ctt
+++ b/examples/prelude.ctt
@@ -36,6 +36,13 @@ inv (A : U) (a b : A) (p : Id A a b) : Id A b a = <i> p @ -i
 compId (A : U) (a b c : A) (p : Id A a b) (q : Id A b c) : Id A a c =
   <i> comp A (p @ i) [ (i = 1) -> q ]
 
+compId' (A : U) (a b c : A) (p : Id A a b) (q : Id A b c) : Id A a c =
+  subst A (Id A a) b c q p
+
+compId'' (A : U) (a b : A) (p : Id A a b) : (c : A) -> (q : Id A b c) -> Id A a c =
+  J A a ( \ (b : A) (p : Id A a b) -> (c : A) -> (q : Id A b c) -> Id A a c) rem b p
+    where rem (c : A) (p : Id A a c) : Id A a c = p
+  
 isoId (A B : U) (f : A -> B) (g : B -> A)
       (s : (y:B) -> Id B (f (g y)) y)
       (t : (x:A) -> Id A (g (f x)) x) : Id U A B =