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'

Fix conv

Merge branch 'master' into csystems

Speed up conv

add some comments in category.ctt and csystem.ctt

rename visible to transparent and fix printing of glue

rename glue -> Glue, glueElem -> glue and unglueElem -> unglue

rename Id to Path

remove nthmUniv

rename Path to PLam and IdP to PathP

make subset compile using opaque

move testempty

merge mult and multS1

move context of indSusp to susp

more duplicate definitions

move ex1 into circle

remove duplicate code

add a line without any specified points

Merge branch 'csystems'

# Conflicts:
# cubicaltt.el
# examples/helix.ctt

don't hardcode list of ctt files in Makefile for generating TAGS file

cleaning in prelude

add equalNat

fix name of local splits

add local split

add batch mode flag

wip

wip on an equivalent presentation of the circle as a quotient of unit

minor changes to circle

Merge pull request #39 from abooij/prop-trunc

implement propositional truncation

Two equivalent categories are equal

wip

wip

Add warning about recursive HITs

Rename truncP to inh

implement propositional truncation

Split csystem.ctt into category.ctt and csystem.ctt

add reserved keywords to README

Construction of a C0-System from a universe category

Fix the module name

(wip) construction of a C0-System from a universe category

Both definitions of C systems; the second one implies the first one

small change

we should improve the evaluator

Merge branch 'master' of github.com:mortberg/cubicaltt into torsor

definition of C systems

Finish binnat example and add elimination principles for equivalences and isomorphisms

simple computation using multZ

torsor multiplication

eval ignores opaqueness
Proof of BZ = (X : (A:U) * (A->A)) * inh (X = (Z, sucZ))

Start porting binnat

visible_all command

Opaque/Visible definitions

some proofs

slow proof

other proof of lemPropF

Only ZEquiv : isEquiv (plus x) is not proven

S1 = BZ

Merge branch 'master' of https://github.com/mortberg/cubicaltt

Z = Id BZ ZBZ ZBZ

.

some computations

study of multiplication on S1

proof that S1 is a groupoid