From 9f29b9acda3069d250bc3da6014f3eddb00f652a Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Sat, 22 Oct 2016 11:56:16 -0400 Subject: [PATCH] update readme --- README.md | 43 +++++++++++++++++++++++++++---------------- 1 file changed, 27 insertions(+), 16 deletions(-) diff --git a/README.md b/README.md index dfe3e5d..a944194 100644 --- a/README.md +++ b/README.md @@ -1,14 +1,16 @@ Cubical Type Theory =================== -Experimental implementation of a cubical type theory in which the user -can directly manipulate n-dimensional cubes. The language extends type -theory with: +Experimental implementation of a [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: * Path abstraction and application * Composition and transport * Equivalences can be transformed into equalities (and univalence can be proved, see "examples/univalence.ctt") +* Identity types (see "examples/idtypes.ctt") * Some higher inductive types (see "examples/circle.ctt" and "examples/integer.ctt") @@ -22,13 +24,17 @@ 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" and "examples/aim.ctt". +For examples, including a demo ("examples/demo.ctt"), see the +[examples](https://github.com/mortberg/cubicaltt/tree/master/examples#cubical-type-theory-examples) +folder. The following keywords are reserved: ``` -module, where, let, in, split, mutual, import, data, hdata, undefined, -IdP, comp, transport, fill, glue, glueElem, unglueElem, U +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 @@ -76,7 +82,7 @@ To run the system type `cubical ` -To enable the debugging mode add the -d flag. In the interaction loop +To see a list of options add the --help flag. In the interaction loop type :h to get a list of available commands. Note that the current directory will be taken as the search path for the imports. @@ -108,21 +114,26 @@ runs it. References and notes -------------------- + * [Cubical Type Theory: a constructive interpretation of the + univalence + axiom](http://www.cse.chalmers.se/~coquand/cubicaltt.pdf), Cyril + Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. This + paper describes the type theory and its model. + +* [Canonicity for Cubical Type + Theory](https://arxiv.org/abs/1607.04156), Simon Huber. Proof of + canonicity for the type theory. + * Voevodsky's lectures and texts on [univalent foundations](http://www.math.ias.edu/vladimir/home) * HoTT book and webpage: [http://homotopytypetheory.org/](http://homotopytypetheory.org/) - * [Cubical Type Theory: a constructive interpretation of the - univalence - axiom](http://www.math.ias.edu/~amortberg/papers/cubicaltt.pdf), - Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg - - * [Cubical Type - Theory](http://www.cse.chalmers.se/~coquand/face.pdf) - The - typing rules of the system. See [this](http://www.cse.chalmers.se/~coquand/face.pdf) - for a variation using isomorphisms instead of equivalences. + * [Cubical Type Theory](http://www.cse.chalmers.se/~coquand/face.pdf) + - Old version of the typing rules of the system. See + [this](http://www.cse.chalmers.se/~coquand/face.pdf) for a + variation using isomorphisms instead of equivalences. * [Internal version of the uniform Kan filling condition](http://www.cse.chalmers.se/~coquand/shape.pdf) -- 2.34.1