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.


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

[Skip to ReadMe]


Versions0.1.0, 0.1.1, 0.1.2, 0.2.0, 0.2.0
Change logNone available
Dependenciesarray (>=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]
AuthorCyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg
CategoryDependent Types
Home page
UploadedSun Apr 27 14:44:15 UTC 2014 by AndersMortberg


Maintainers' 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 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: