From 0a1c34d467741dcb0198fd0bb6ec0599b0deec93 Mon Sep 17 00:00:00 2001
From: coquand <coquand@chalmers.se>
Date: Tue, 14 Apr 2015 13:31:43 +0200
Subject: [PATCH] added some lines in ex1.ctt

---
 examples/ex1.ctt | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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
 
-- 
2.34.1