From 596753f4289afd5711b7ab7ae53a32f64b697729 Mon Sep 17 00:00:00 2001 From: Anders Date: Fri, 27 Mar 2015 17:55:14 +0100 Subject: [PATCH] fix readme --- README.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 910c07f..4e19ea3 100644 --- a/README.md +++ b/README.md @@ -14,9 +14,9 @@ Because of this it is not necessary to have a special file of 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` +`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` Install -- 2.34.1