From: Anders Date: Fri, 27 Mar 2015 16:57:45 +0000 (+0100) Subject: readme X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=e053ab35dfa94b713ad7bf7246f759f39a994471;p=cubicaltt.git readme --- diff --git a/README.md b/README.md index d0a9a21..5cfe325 100644 --- a/README.md +++ b/README.md @@ -14,12 +14,11 @@ 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 -------