Skip to content

Latest commit

 

History

History
166 lines (117 loc) · 4.85 KB

README.md

File metadata and controls

166 lines (117 loc) · 4.85 KB

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".

The following keywords are reserved:

module, where, let, in, split, mutual, import, data, hdata, undefined,
IdP, comp, transport, fill, glue, glueElem, unglueElem, U

Install

To compile the project using cabal, first install the build-time dependencies (either globally or in a cabal sandbox):

cabal install alex happy bnfc

Then the project can be built (and installed):

cabal install

Alternatively, a Makefile is provided:

    make

This assumes that the following Haskell packages are installed using cabal:

mtl, haskeline, directory, BNFC, alex, happy, QuickCheck

To build the TAGS file, run:

    make TAGS

This assumes that hasktags has been installed.

To clean up, run:

    make clean

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.

When using cabal sandboxes, cubical can be invoked using

cabal exec cubical <filename>

To enable emacs to edit *.ctt files in ctt-mode, add the following line to your .emacs file:

(autoload 'ctt-mode "cubicaltt" "cubical editing mode" t)
(setq auto-mode-alist (append auto-mode-alist '(("\\.ctt$" . ctt-mode))))

and ensure that the file cubicaltt.el is visible in one of the diretories on emacs' load-path, or else load it in advance, either manually with M-x load-file, or with something like the following line in .emacs:

(load-file "cubicaltt.el")

References and notes

Authors

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