Update README

diff --git a/README.md b/README.md
index 9e14dea9945540d987f329ada7377758956ee38f..7aa0b449c8b0e21150ef50b1525e33eee293377f 100644 (file)
--- a/README.md
+++ b/README.md
@@ -12,8 +12,8 @@ theory with:
   "examples/susp.ctt")
 
 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:
+primitives (like in [cubical](https://github.com/simhu/cubical), for
+instance function extensionality is provable in the system by:
 
 ```
 funExt (A : U) (B : A -> U) (f g : (x : A) -> B x)
@@ -25,7 +25,6 @@ This proof can be compared with the one in "examples/funext.ctt" which
 proves that univalence implies function extensionality (the normal
 form of these proofs are almost the same).
 
-
 For more examples, see "examples/demo.ctt".
 
 
@@ -56,39 +55,45 @@ directory will be taken as the search path for the imports.
 References and notes
 --------------------
 
- * Voevodsky's home page on univalent foundation
+ * [A Cubical Type
+   Theory](http://www.cse.chalmers.se/~coquand/rules5.pdf) -
+   The typing rules of the system
+
+ * Voevodsky's page on [univalent
+   foundations](http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations.html)
 
  * HoTT book and webpage:
    [http://homotopytypetheory.org/](http://homotopytypetheory.org/)
 
- * [A Cubical Type
-   Theory](http://www.cse.chalmers.se/~coquand/rules5.pdf) -
-   Presenting typing rules of the system
-
  * [A Cubical Approach to Synthetic Homotopy
-    Theory][http://dlicata.web.wesleyan.edu/pubs/lb15cubicalsynth/lb15cubicalsynth.pdf),
-    Dan Licata, Guillaume Brunerie.
+   Theory][http://dlicata.web.wesleyan.edu/pubs/lb15cubicalsynth/lb15cubicalsynth.pdf),
+   Dan Licata, Guillaume Brunerie.
 
- * Type Theory in Color, J.P. Bernardy, G. Moulin
+ * [Type Theory in
+   Color](http://www.cse.chalmers.se/~bernardy/CCCC.pdf),
+   Jean-Philippe Bernardy, Guilhem Moulin.
 
- * A simple type-theoretic language: Mini-TT, Th. Coquand,
-   Y. Kinoshita, B. Nordström and M. Takeyama
+ * [A simple type-theoretic language:
+   Mini-TT](http://www.cse.chalmers.se/~bengt/papers/GKminiTT.pdf),
+   Thierry Coquand, Yoshiki Kinoshita, Bengt Nordström and Makoto
+   Takeyama - This presents the type theory that the system is based
+   on.
 
  * [A cubical set model of type
-   theory](http://www.cse.chalmers.se/~coquand/model1.pdf), M. Bezem,
-   Th. Coquand and S. Huber.
+   theory](http://www.cse.chalmers.se/~coquand/model1.pdf), Marc
+   Bezem, Thierry Coquand and Simon Huber.
 
  * [An equivalent presentation of the Bezem-Coquand-Huber category of
-   cubical sets](http://arxiv.org/abs/1401.7807), A. Pitts.
-
-   This gives a presentation of the cubical set model in nominal sets.
+   cubical sets](http://arxiv.org/abs/1401.7807), Andrew Pitts - This
+   gives a presentation of the cubical set model in nominal sets.
 
  * [Remark on singleton
-   types](http://www.cse.chalmers.se/~coquand/singl.pdf), Th. Coquand.
+   types](http://www.cse.chalmers.se/~coquand/singl.pdf), Thierry
+   Coquand.
 
  * [Note on Kripke
-   model](http://www.cse.chalmers.se/~coquand/countermodel.pdf), M. Bezem
-   and Th. Coquand.
+   model](http://www.cse.chalmers.se/~coquand/countermodel.pdf), Marc
+   Bezem and Thierry Coquand.
 
 
 Authors