From: coquand <coquand@chalmers.se>
Date: Tue, 14 Apr 2015 11:31:43 +0000 (+0200)
Subject: added some lines in ex1.ctt
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=0a1c34d467741dcb0198fd0bb6ec0599b0deec93;p=cubicaltt.git

added some lines in ex1.ctt
---

diff --git a/examples/ex1.ctt b/examples/ex1.ctt
index 08360b7..9069833 100644
--- 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