From 812c0e7f536b2ebfd7944cc7d8d8fd853c00848e Mon Sep 17 00:00:00 2001 From: Anders Date: Mon, 13 Apr 2015 15:01:59 +0200 Subject: [PATCH] Update README --- README.md | 47 ++++++++++++++++++++++++++--------------------- 1 file changed, 26 insertions(+), 21 deletions(-) diff --git a/README.md b/README.md index 9e14dea..7aa0b44 100644 --- 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 -- 2.34.1