cubical: Implementation of Univalence in Cubical Sets

This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.

[maintain] [Publish]

Cubical implements an experimental simple type checker for type theory with univalence with an evaluator for closed terms.


[Skip to Readme]

Properties

Versions 0.1.0, 0.1.1, 0.1.2, 0.2.0, 0.2.0
Change log None available
Dependencies array (>=0.4), base (>=4.5 && <5), BNFC (>=2.5), directory (>=1.2), filepath (>=1.3), haskeline (>=0.7), mtl (>=2.1), transformers (>=0.3) [details]
License MIT
Author Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg
Maintainer mortberg@chalmers.se
Category Dependent Types
Home page https://github.com/simhu/cubical
Uploaded by AndersMortberg at 2014-04-27T14:44:15Z

Downloads

Maintainer's Corner

For package maintainers and hackage trustees


Readme for cubical-0.2.0

[back to package description]

CUBICAL

Cubical implements an experimental simple type-checker for type theory with univalence with an evaluator for closed terms.

INSTALL

To install cubical, a working Haskell and cabal installation are required. To build cubical go to the main directory and do

cabal install

To only build (not install) cubical do

cabal configure

cabal build

Alternatively one can also use the Makefile to build the system by typing:

make bnfc && make

However this requires that the following Haskell packages are installed:

mtl, haskeline, directory, BNFC, alex, happy

Note: In order to make the mutual keyword work a patched version of BNFC is needed. To install this download the patched version from

https://github.com/simhu/bnfc

and then cabal install it.

###Emacs mode:

To install syntax highlighting for cubical files load the cubical.el file into emacs. In order to load it automatically add

(load-file "/path/to/cubical.el")

(add-to-list 'auto-mode-alist '("\\.cub\\'" . cub-mode))

to your .emacs file.

USAGE

To run cubical 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.

OVERVIEW

The program is organized as follows:

During type-checking, we consider the primitives listed in examples/primitive.cub as non interpreted constants. The type-checker is in the file TypeChecker.hs and is rudimentary (200 lines), without good error messages.

These primitives however have a meaning in cubical sets, and the evaluation function computes this meaning. This semantics/evaluation is described in the file Eval.hs, which is the main file. The most complex part corresponds to the computations witnessing that the universe has Kan filling operations.

For writing this semantics, it was convenient to use the alternative presentation of cubical sets as nominal sets with 01-substitutions (see A. Pitts' note, references listed below).

The primitives needed to get univalence are.

DESCRIPTION OF THE LANGUAGE

We have

The syntax allows Landin's offside rule similar to Haskell.

The basic (untyped) language has a direct simple denotational semantics. Type theory works with the total part of this language (it is possible to define totality at the denotational semantics level). Our evaluator works in a nominal version of this semantics. The type-checker assumes that we work in this total part, however, there is no termination check.

DESCRIPTION OF THE SEMANTICS/EVALUATION

The values depend on a new class of names, also called directions, which can be thought of as varying over the unit interval [0,1]. A path connecting a0 and a1 in the direction x is a value p(x) such that p(0) = a0 and p(1) = a1. An element in the identity type a0 = a1 is then of the form <x>p(x) where the name x is bound. An identity proof in an identity type will then be interpreted as a "square" of the form <x><y>p(x,y). See examples/hedberg.cub and the example test3 (in the current implementation directions/names are represented by numbers).

Operationally, a type is explained by giving what are its Kan filling operation. For instance, we have to explain what are the Kan filling for the dependent product.

The main step for interpreting univalence is to transform an equivalence A -> B to a path in any direction x connecting A and B. This is a new basic element of the universe, called VEquivEq in the file Eval.hs which takes a name and arguments A,B,f and the proof that f is an equivalence. The main part of the work is then to explain the Kan filling operation for this new type.

The Kan filling for the universe can be seen as a generalization of the operation of composition of relation.

DESCRIPTION OF THE EXAMPLES

The directory examples contains some examples of proofs. The file examples/primitive.cub list the new primitives that have cubical set semantics. These primitive notions imply the axiom of univalence. The file examples/primitive.cub should be the basis of any development using univalence.

Most of the example files contain simple test examples of computations:

NEWS (to be detailed)

FURTHER WORK (non-exhaustive)

REFERENCES AND NOTES

AUTHORS

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