Fix examples

diff --git a/examples/equiv.ctt b/examples/equiv.ctt
index 4beebb5265d4211d6b799e2346a159529639b601..ef097f29835e618d345c2f01302f2ab63fc36207 100644 (file)
--- a/examples/equiv.ctt
+++ b/examples/equiv.ctt
@@ -63,6 +63,6 @@ lemEquivFib (A:U) (F G :A -> U) (f:(x:A) -> F x -> G x)
       where yu : AF = z.1\r
             y : A = yu.1\r
             w : F y = yu.2\r
-            p : Id A x y = <i>(rem3 @ i).1\r
+            p : Id A x y = <i>(z.2 @ i).1\r
             q : IdP (<j>G (p@j)) v (f y w) = <i>((z.2) @ i).2\r
    rem7 (z0 z1 : fiber (F x) (G x) (f x) v) : Id (fiber (F x) (G x) (f x) v) z0 z1 = <i>psi ((rem1.1 (phi z0) (phi z1))@i)\r

diff --git a/examples/integer.ctt b/examples/integer.ctt
index 57c5db258910b5008e978a52131ead29412fa95a..6e3ed0c7725cf927eeb2fe7e303d765a3f965b38 100644 (file)
--- a/examples/integer.ctt
+++ b/examples/integer.ctt
@@ -26,9 +26,9 @@ predInt : int -> int = split
 
 toZ : int -> Z = split
   pos n -> inr n
-  neg n -> fun n
-    where fun : nat -> Z = split
-      zero -> zeroZ
+  neg n -> auxToZ n
+    where auxToZ : nat -> Z = split
+      zero -> inr zero
       suc n -> inl n
   zeroP @ i -> zeroZ