From 32dbb48584d8e8c05e8b266295b22f2a4dfd165b Mon Sep 17 00:00:00 2001 From: Anders Date: Fri, 27 Mar 2015 17:55:51 +0100 Subject: [PATCH] fix readme --- README.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/README.md b/README.md index 4e19ea3..d0a9a21 100644 --- a/README.md +++ b/README.md @@ -15,7 +15,9 @@ primitives (like in cubical), for instance function extensionality is provable in the system by: `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` -- 2.34.1