From: Anders Mörtberg <mortberg@chalmers.se>
Date: Tue, 21 Apr 2015 08:10:51 +0000 (+0200)
Subject: Fix examples
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=fd54a6d0e5bc702a7646e698a9d7d75c39f86dfc;p=cubicaltt.git

Fix examples
---

diff --git a/examples/equiv.ctt b/examples/equiv.ctt
index 4beebb5..ef097f2 100644
--- 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
             y : A = yu.1
             w : F y = yu.2
-            p : Id A x y = <i>(rem3 @ i).1
+            p : Id A x y = <i>(z.2 @ i).1
             q : IdP (<j>G (p@j)) v (f y w) = <i>((z.2) @ i).2
    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)
diff --git a/examples/integer.ctt b/examples/integer.ctt
index 57c5db2..6e3ed0c 100644
--- 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