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'

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