From 8c35d190eb1d2a41389d6befffa6295577ba2e51 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Sat, 22 Oct 2016 11:58:10 -0400 Subject: [PATCH] README --- README.md | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index a944194..9281cf0 100644 --- a/README.md +++ b/README.md @@ -1,7 +1,7 @@ Cubical Type Theory =================== -Experimental implementation of a [Cubical Type +Experimental implementation of [Cubical Type Theory](http://www.cse.chalmers.se/~coquand/cubicaltt.pdf) in which the user can directly manipulate n-dimensional cubes. The language extends type theory with: @@ -16,7 +16,7 @@ extends type theory with: Because of this it is not necessary to have a special file of primitives (like in [cubical](https://github.com/simhu/cubical)), for -instance function extensionality is provable in the system by: +instance function extensionality is directly provable in the system: ``` funExt (A : U) (B : A -> U) (f g : (x : A) -> B x) @@ -34,7 +34,6 @@ The following keywords are reserved: module, where, let, in, split, with, mutual, import, data, hdata, undefined, PathP, comp, transport, fill, Glue, glue, unglue, U, opaque, transparent, transparent_all, Id, idC, idJ - ``` Install @@ -59,7 +58,9 @@ Alternatively, a `Makefile` is provided: This assumes that the following Haskell packages are installed using cabal: +``` mtl, haskeline, directory, BNFC, alex, happy, QuickCheck +``` To build the TAGS file, run: -- 2.34.1