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:

• Path abstraction and application
• Composition and transport
• Equivalences can be transformed into equalities (and univalence can be proved, see "examples/univalence.ctt")
• Some higher inductive types (see "examples/circle.ctt" and "examples/integer.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:

funExt (A : U) (B : A -> U) (f g : (x : A) -> B x)
       (p : (x : A) -> Id (B x) (f x) (g x)) :
       Id ((y : A) -> B y) f g = <i> \(a : A) -> (p a) @ i

For more examples, see "examples/demo.ctt" and "examples/aim.ctt".

Install

To compile the program type:

make bnfc && make

This assumes that the following Haskell packages are installed:

mtl, haskeline, directory, BNFC, alex, happy

Usage

To run the system type

cubical <filename>

To enable the debugging mode add the -d 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.

References and notes

• Voevodsky's lectures and texts on univalent foundations

• HoTT book and webpage: http://homotopytypetheory.org/

• Cubical Type Theory - The typing rules of the system

• Internal version of the uniform Kan filling condition

• A category of cubical sets - main definitions towards a formalization

• hoq - A language based on homotopy type theory with an interval (documentation available here).

• A Cubical Approach to Synthetic Homotopy Theory, Dan Licata, Guillaume Brunerie.

• Type Theory in Color, Jean-Philippe Bernardy, Guilhem Moulin.

• A simple type-theoretic language: Mini-TT, 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, Marc Bezem, Thierry Coquand and Simon Huber.

• An equivalent presentation of the Bezem-Coquand-Huber category of cubical sets, Andrew Pitts - This gives a presentation of the cubical set model in nominal sets.

• Remark on singleton types, Thierry Coquand.

• Note on Kripke model, Marc Bezem and Thierry Coquand.

Authors

Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg