From 19ab11cc9b2ffe5b62d72806b3ee023fb84b4c55 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Fri, 3 Jul 2015 10:02:49 +0200 Subject: [PATCH] Update README --- README.md | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 8e983d0..48acfff 100644 --- a/README.md +++ b/README.md @@ -22,7 +22,7 @@ funExt (A : U) (B : A -> U) (f g : (x : A) -> B x) Id ((y : A) -> B y) f g = \(a : A) -> (p a) @ i ``` -For more examples, see "examples/demo.ctt". +For more examples, see "examples/demo.ctt" and "examples/aim.ctt". Install @@ -59,9 +59,16 @@ References and notes [http://homotopytypetheory.org/](http://homotopytypetheory.org/) * [Cubical Type - Theory](http://www.cse.chalmers.se/~coquand/rules5.pdf) - The + Theory](http://www.cse.chalmers.se/~coquand/rules7.pdf) - The typing rules of the system + * [Internal version of the uniform Kan filling + condition](http://www.cse.chalmers.se/~coquand/shape.pdf) + + * [A category of cubical + sets](http://www.cse.chalmers.se/~coquand/vv.pdf) - main + definitions towards a formalization + * [Lecture Notes on Cubical sets](http://www.cse.chalmers.se/~coquand/course3.pdf) -- 2.34.1