From: Anders Mörtberg <mortberg@chalmers.se>
Date: Sat, 6 Jun 2015 09:23:12 +0000 (+0200)
Subject: Update aim.ctt again
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=4066ab922bb8e69238f39b676417779d23651402;p=cubicaltt.git

Update aim.ctt again
---

diff --git a/examples/aim.ctt b/examples/aim.ctt
index 889092c..babd5cc 100644
--- a/examples/aim.ctt
+++ b/examples/aim.ctt
@@ -116,7 +116,7 @@ funExt (A : U) (B : A -> U) (f g : (x : A) -> B x)
        (p : (x : A) -> Id (B x) (f x) (g x)) : Id ((y : A) -> B y) f g =
   <i> \(a : A) -> (p a) @ i
 
-{- 
+{-
 
 To see that the definition of funExt makes sense we can compute its
 faces:
@@ -637,14 +637,14 @@ intSet : set int = subst U set Z int isoIntZ ZSet
 --------------------------------------------------------------------------
 
   o Definitional equality for J? Problem pointed out by Dan Licata
-    with regularity for composition in the universe. However the
-    system seems to work without regularity (this is work in
-    progress).
+    with regularity for composition in the universe. However, the
+    system might still work without regularity (this is what is being
+    implemented in the no_regular branch).
 
   o Meta-theoretical properties of the system and correctness of the
     model. Formalization?
 
-  o Integration of ideas into other proof assistants (eg Agda)?
+  o Integration of ideas into other proof assistants (e.g. Agda)?
 
 -}
 
@@ -658,6 +658,7 @@ addZero : (a : nat) -> Id nat (add zero a) a = split
 
 addCom (a : nat) : (b : nat) -> Id nat (add a b) (add b a) = split
   zero   -> <i> addZero a @ -i
-  suc b' -> <i> comp nat (suc (addCom a b' @ i)) [ (i = 0) -> <j> suc (add a b')
-                                                 , (i = 1) -> <j> addSuc b' a @ -j ]
+  suc b' -> <i> comp (<_> nat) (suc (addCom a b' @ i)) [ (i = 0) -> <j> suc (add a b')
+                                                       , (i = 1) -> <j> addSuc b' a @ -j ]
+
 -}