by mortberg

mortberg / cubicaltt

Experimental implementation of Cubical Type Theory

435 Stars 71 Forks Last release: Not found MIT License 688 Commits 1 Releases

Available items

No Items, yet!

The developer of this repository has not created any items for sale yet. Need a bug fixed? Help with integration? A different license? Create a request here:

Cubical Type Theory

Experimental implementation of 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")
  • Identity types (see "examples/idtypes.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 directly provable in the system:

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 =  \(a : A) -> (p a) @ i

For examples, including a demo ("examples/demo.ctt"), see the examples folder. For a summary of where to find the main results of the cubical type theory paper in the examples folder see "examples/summary.ctt".

The following keywords are reserved:

module, where, let, in, split, with, mutual, import, data, hdata,
undefined, PathP, comp, transport, fill, Glue, glue, unglue, U,
opaque, transparent, transparent_all, Id, idC, idJ


You can compile the project using either

, or


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

is provided:

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

has been installed.

To clean up, run:

    make clean


To compile and install the project using stack, run:

    stack setup
    stack install


To run the system type


To see a list of options add the --help 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,

can be invoked using

cabal exec cubical 

To enable emacs to edit

files in
, add the following line to your
(autoload 'cubicaltt-mode "cubicaltt" "cubical editing mode" t)
(setq auto-mode-alist (append auto-mode-alist '(("\\.ctt$" . cubicaltt-mode))))
and ensure that the file
is visible in one of the diretories on emacs'
, or else load it in advance, either manually with
M-x load-file
, or with something like the following line in
(load-file "cubicaltt.el")

When using

in Emacs, the command
will launch the interactive toplevel in an Emacs buffer and load the current file. It is bound to
C-c C-l
by default. If
is not on Emacs's
, then set the variable
to the command that runs it.

References and notes


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

We use cookies. If you continue to browse the site, you agree to the use of cookies. For more information on our use of cookies please see our Privacy Policy.