* 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
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
-------
* 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,
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.
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
-------
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
-module talk where
+module demo where
-- Cubical type theory!
-----------------------
| 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