projects
/
cubicaltt.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
6468024
)
fix readme
author
Anders
<mortberg@chalmers.se>
Fri, 27 Mar 2015 16:55:14 +0000
(17:55 +0100)
committer
Anders
<mortberg@chalmers.se>
Fri, 27 Mar 2015 16:55:14 +0000
(17:55 +0100)
README.md
patch
|
blob
|
blame
|
history
diff --git
a/README.md
b/README.md
index 910c07f783bc45259c26195e1af7145c8ced3478..4e19ea30a06efe506b26c4a529d9a10f895c00fe 100644
(file)
--- 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 = <i> \(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 = <i> \(a : A) -> (p a) @ i`
Install