From c2903f1f6ffa8da792353343e03f095b88b78d21 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Sat, 6 Jun 2015 11:18:14 +0200 Subject: [PATCH] Update aim.ctt --- examples/aim.ctt | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) 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 = \(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. + +-} {- -- 2.34.1