Experimental implementation of Cubical Type Theory

Available items

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**:

Readme

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

cabal,

make, or

stack.

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

Makefileis 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

hasktagshas 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

cubical

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,

cubicalcan be invoked using

cabal exec cubical

To enable emacs to edit

*.cttfiles in

cubicaltt-mode, add the following line to your

.emacsfile:

(autoload 'cubicaltt-mode "cubicaltt" "cubical editing mode" t) (setq auto-mode-alist (append auto-mode-alist '(("\\.ctt$" . cubicaltt-mode))))and ensure that the file

cubicaltt.elis 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")

When using

cubicaltt-modein Emacs, the command

cubicaltt-loadwill launch the interactive toplevel in an Emacs buffer and load the current file. It is bound to

C-c C-lby default. If

cubicalis not on Emacs's

exec-path, then set the variable

cubicaltt-commandto the command that runs it.

Cubical Type Theory: a constructive interpretation of the univalence axiom, Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. This paper describes the type theory and its model.

Canonicity for Cubical Type Theory, Simon Huber. Proof of canonicity for the type theory.

Voevodsky's lectures and texts on univalent foundations

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

Cubical Type Theory - Old version of the typing rules of the system. See this for a variation using isomorphisms instead of equivalences.

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.

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