Update aim.ctt

diff --git a/examples/aim.ctt b/examples/aim.ctt
index 22b1e0ea95fb2ece695279b46c875ccb9edb7a25..889092c48bb496e383963c0137c3464191fb512b 100644 (file)
--- a/examples/aim.ctt
+++ b/examples/aim.ctt
@@ -116,11 +116,18 @@ 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 the definition of funExt makes sense we can compute its faces:
---
--- funExt @ 0 = \(a : A) -> (p a) @ 0      (faces commute with operations)
---            = \(a : A) -> f a            (p a proves Id (B a) (f a) (g a))
---            = f                          (by eta)
+{- 
+
+To see that the definition of funExt makes sense we can compute its
+faces:
+
+funExt @ 0 = \(a : A) -> (p a) @ 0
+           = \(a : A) -> f a
+           = f
+
+The last equality holds because of eta.
+
+-}
 
 
 {-