From: Anders <mortberg@chalmers.se>
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 = <i> \(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 = <i> square (l @ i)
-tripleLoop (l : loopS1) : loopS1 = <i> mult (l @ i) (square (l @ i))
\ No newline at end of file
+tripleLoop (l : loopS1) : loopS1 = <i> mult (l @ i) (square (l @ i))
+
+triv : loopS1 = <i> base
+
+-- A nice example
+hmtpy : Id loopS1 triv (<i> loop{S1} @ (i /\ -i)) = <j 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
 -- "<i>" abstracts the name/color/dimension i.
 Id (A : U) (a b : A) : U = IdP (<i> A) a b
 
-
 refl (A : U) (a : A) : Id A a a = <i> a
--- \(i : Interval) -> ... for <i> ..
 
 
 inv (A : U) (a b : A) (p : Id A a b) : Id A b a = <i> 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)