general constcubes 2-3-4D

constcubes in n dimensions

add first version of lecture 4

Merge pull request #66 from mortberg/shadowed

Check if some names were shadowed while loading a file

move test up

remove empty lines

Check if some names were shadowed while loading the file

fix typos

add lecture 3

minor

minor

minor update to lecture 2

Add lecture 2

update lecture1

lecture1

update lecture

first lecture

Allow overlapping Arbitrary for Face and System

Boxing Env to prevent Show conflicts with newer versions of haskell packages

minor change

Merge pull request #60 from Rotsor/more-parens-in-goal

More parentheses when printing values

Merge pull request #59 from Rotsor/checkPLam-error-message

better error message from checkPLam

Fix printing of idC and idJ also for values

Don't use smart-constructors when normalizing values

Show idC and idJ as we parse them

More parentheses when printing values

Fixes a bug where not enough parentheses would be printed.
Previously if a function F is defined by split, `F (F x)` would be printed as `F F x`.
Now it's printed as `F (F x)` as it should.

better error message from checkPLam

Merge pull request #58 from Rotsor/patch-1

Emacs mode: ignore backslash character

Emacs mode: ignore backslash character

Emacs treats the '\' as an escape character by default, which means it sees `\(foo : x) -> bar` as having unbalanced parentheses and therefore `forward-sexp` and related functions don't work.

minor changes to bool

experiment with Id

Merge pull request #56 from linuborj/cubicaltt_grothendieck

Added a formalisation of the Grothendieck group and a proof that a family of universal arrows gives rise to an adjunction.

Uncommented slow function.

Added definitions of algebraic structures in algstruct.ctt, a construction of the Grothendieck group in grothendieck.cct, definitions of natural transformations, universal arrows, and adjunctions in univprop as well as a proof that a family of universal arrows gives rise to an adjunction.

swap direction of equality to match order in comment

add opposite category

add a comment to category

readme

update demo

readme

readme

README

update readme

doc

doc

test

test

add a readme for the examples folder

add summary file

doc

move graph script

comment

add a script for loading all files

comments

move implicit point

a lot of comments

remove undefined and make csystem compile

comments

update category

comments

add transparent_all to keywords in emacs file

remove examples/aim.ctt as it is subsumed by examples/demo.ctt

add a small puzzle due to Andrew Polonsky

Merge pull request #49 from mortberg/defeqJ

Add Id types

Fix insertSystem to maintain invariant for systems

Closes #52.

cleaning

cleaning

visible -> transparent

direct definition of retract

add Dan's proof of univalence from ua and uabeta

Merge pull request #50 from david-christiansen/elisp-conventions

Emacs mode updates

Emacs mode: Update names for Customize

Now Customize uses the updated names consistently.

Update README for Emacs mode

Remove redundant comment command from Emacs mode

It is sufficient to set a couple of variables to make the built-in
commenting command work for cubical.

Remove CL-isms from Emacs mode

*foo* is Common Lisp for special variables, while foo is Emacs Lisp for
 the same.

Rename Emacs mode identifiers

Now, the identifiers match the mode filename, per Elisp convention.

Better comment about space-escaping in Emacs mode

The behavior of :cd at the cubical shell is now better described in a
comment, so as to not surprise Elisp hackers.

define equivalence using Id and prove univalence with Id everywhere

minor changes

cleaning and a version of univalence for Id

rename Eq to Id

Some experiments with Eq

Added Eq types with definitional equality for J

Merge pull request #46 from david-christiansen/elisp-conventions

Emacs mode: completion, imenu, and friendlier Customize

Merge pull request #45 from david-christiansen/emacs-update

Add subprocess to Emacs mode

Merge pull request #44 from gullcomb/opt-decl-cmp

Speed up comparison of environments

change back conversion

Merge branch 'conv'

Improve the display of Emacs customize

The customization options in Emacs are now shown with friendlier names.

Add imenu support to the Emacs mode

imenu is a general-purpose index for things in a buffer, used by a
variety of Emacs tools to give a list of definitions in the buffer.
This adds support for it to the Emacs mode.

Add support for completion

Define a completion function and add it to completion-at-point-functions
in ctt-mode. This function is used by many different completion systems
in Emacs, including company-mode and the built-in simple
completion-at-point.

Completion uses a regexp to attempt to find names defined in the current
buffer as well as using the language keywords as sources of completion.

Make the Emacs mode work for package.el

Modify the Emacs mode to make it follow typical Elisp conventions, as
well as adding the necessary headers to make it work in the package
system.

Additionally, the mode is now derived from prog-mode, which will enable
hooks that should work for all programming language modes to run.

Add subprocess to Emacs mode

The Emacs mode for cubical can now run cubical as a subprocess. The
keybinding "C-c C-l", which is the same as Agda and Idris, saves the
current buffer and loads it in cubical.

Additionally, a Customize setting is added to allow users to easily
customize the command to be used to invoke cubical.

minor changes

Tag declarations with their location.

This speeds up the comparison of environments in the common case of
identical declarations.

Fix build for GHC 7.8

This version does not implement the Foldable/Traversable in Prelude
proposal thus `elem` does not work on Sets.

fix bug in printing

cleaning of binnat

Clean up of univalence and add the definition of univalence using the map defined using J

Merge branch 'csystems'