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

Update aim.ctt
---

diff --git a/examples/aim.ctt b/examples/aim.ctt
index 22b1e0e..889092c 100644
--- 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.
+
+-}
 
 
 {-