From: Anders Date: Mon, 13 Apr 2015 12:55:24 +0000 (+0200) Subject: Update the README and examples X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=4b971fd38c6557b81116f7bb22952752d188b907;p=cubicaltt.git Update the README and examples --- diff --git a/README.md b/README.md index 5cfe325..9e14dea 100644 --- a/README.md +++ b/README.md @@ -8,7 +8,8 @@ theory with: * Path abstraction and application * Composition and transport * Isomorphisms can be transformed into equalities -* Some higher inductive types +* Some higher inductive types (see "examples/circle.ctt" and + "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 @@ -20,6 +21,14 @@ funExt (A : U) (B : A -> U) (f g : (x : A) -> B x) Id ((y : A) -> B y) f g = \(a : A) -> (p a) @ i ``` +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". + + Install ------- @@ -52,6 +61,14 @@ References and notes * 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. + * Type Theory in Color, J.P. Bernardy, G. Moulin * A simple type-theoretic language: Mini-TT, Th. Coquand, @@ -61,11 +78,6 @@ References and notes theory](http://www.cse.chalmers.se/~coquand/model1.pdf), M. Bezem, Th. Coquand and S. Huber. - * [A remark on contractible family of - type](http://www.cse.chalmers.se/~coquand/contr.pdf), Th. Coquand. - - This note explains how to derive univalence. - * [An equivalent presentation of the Bezem-Coquand-Huber category of cubical sets](http://arxiv.org/abs/1401.7807), A. Pitts. @@ -78,10 +90,6 @@ References and notes model](http://www.cse.chalmers.se/~coquand/countermodel.pdf), M. Bezem and Th. Coquand. - * [Some connections between cubical sets and - parametricity](http://www.cse.chalmers.se/~coquand/param.pdf), - Th. Coquand. - Authors ------- diff --git a/examples/circle.ctt b/examples/circle.ctt index b753115..d7a0a17 100644 --- a/examples/circle.ctt +++ b/examples/circle.ctt @@ -37,4 +37,9 @@ mult (x : S1) : S1 -> S1 = split square (x : S1) : S1 = mult x x doubleLoop (l : loopS1) : loopS1 = square (l @ i) -tripleLoop (l : loopS1) : loopS1 = mult (l @ i) (square (l @ i)) \ No newline at end of file +tripleLoop (l : loopS1) : loopS1 = mult (l @ i) (square (l @ i)) + +triv : loopS1 = base + +-- A nice example +hmtpy : Id loopS1 triv ( loop{S1} @ (i /\ -i)) = loop{S1} @ j /\ i /\ -i \ No newline at end of file diff --git a/examples/talk.ctt b/examples/demo.ctt similarity index 97% rename from examples/talk.ctt rename to examples/demo.ctt index 8edc441..e4b6f1b 100644 --- a/examples/talk.ctt +++ b/examples/demo.ctt @@ -1,4 +1,4 @@ -module talk where +module demo where -- Cubical type theory! ----------------------- @@ -27,13 +27,11 @@ data list (A : U) = nil | cons (a : A) (as : list A) --- IdP is a built-in notion. +-- "IdP P a b" is a built-in notion where P : Id U A B, a : A and b : B -- "" abstracts the name/color/dimension i. Id (A : U) (a b : A) : U = IdP ( A) a b - refl (A : U) (a : A) : Id A a a = a --- \(i : Interval) -> ... for .. inv (A : U) (a b : A) (p : Id A a b) : Id A b a = p @ -i diff --git a/examples/funext.ctt b/examples/funext.ctt index f2ed6f1..60e50f5 100644 --- a/examples/funext.ctt +++ b/examples/funext.ctt @@ -2,6 +2,9 @@ module funext where import prelude +-- Proof that univalence implies funtion extensionality based on: +-- http://homotopytypetheory.org/2014/02/17/another-proof-that-univalence-implies-function-extensionality/ + homotopies (A B :U) : U = (fg : (_:A->B) * (A->B)) * (x:A) -> Id B (fg.1 x) (fg.2 x)