readme

diff --git a/README.md b/README.md
index d0a9a2167421e63273896da4029fd83a8ec1d452..5cfe3256fc609eccb572fa9fd4c55ac3bcd48585 100644 (file)
--- 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 = <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
 -------