From 4b5df5854862642bc1c3c9bb99a31c63961aaf33 Mon Sep 17 00:00:00 2001 From: Anders Date: Mon, 13 Apr 2015 15:18:15 +0200 Subject: [PATCH] Update README --- README.md | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index c772ff0..dd14e2f 100644 --- a/README.md +++ b/README.md @@ -12,7 +12,7 @@ theory with: "examples/susp.ctt") Because of this it is not necessary to have a special file of -primitives (like in [cubical](https://github.com/simhu/cubical), for +primitives (like in [cubical](https://github.com/simhu/cubical)), for instance function extensionality is provable in the system by: ``` @@ -59,6 +59,9 @@ References and notes Theory](http://www.cse.chalmers.se/~coquand/rules5.pdf) - The typing rules of the system + * [Lecture Notes on Cubical + sets](http://www.cse.chalmers.se/~coquand/course1.pdf) + * Voevodsky's page on [univalent foundations](http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations.html) -- 2.34.1