Add the circle (there is a bug)

diff --git a/examples/circle.ctt b/examples/circle.ctt
new file mode 100644 (file)
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 (file)
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 51c1594b445a4f4bc330805e7692206fd5eff5d6..4abdb03cd214fc3f59aaef443e3d52d233ef75fd 100644 (file)
--- 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 =