added some lines in ex1.ctt

diff --git a/examples/ex1.ctt b/examples/ex1.ctt
index 08360b74fc36e1465f2104e3a9f00e7d12a5e829..90698331239672ef0b8e2389dbfb043d0e297fec 100644 (file)
--- a/examples/ex1.ctt
+++ b/examples/ex1.ctt
@@ -27,7 +27,7 @@ thm (X A:U) : Id U ((f:X->A) * constant X A f) (S X -> A) = isoId T0 T1 f g t s
        s (x:T0) : Id T0 (g (f x)) x = refl T0 x
        t : (y:T1) -> Id T1 (f (g y)) y = lem X A
 
--- a special case
+-- a special case, Lemmas 6.2.5-6.2.9 in the book
 
 aLoop (A:U) : U = (a:A) * Id A a a