Move to haskell 2010

Populate extra-source-files

Complete cubicaltt.cabal: list all generated modules, improve syntax.

Rename executable to cubical (as in Makefile)

Converted the project into a cabal project.

Using the cabal project files, one can easily build this project in sandboxes.
It is also more easy to package for distribution.

Also includes a minor LICENSE file reformatting and encoding fix.

Original Makefile is still in place.

Reintroduce hdata

Removed unGlue

Merge branch 'mutual'

Rename Simple into NonMutual and added sanity check

updated README

Fixed and added comment for transpHIT

Reintroduced mutual (wip)

Fix squeezes

Merge pull request #14 from vladimirias/master

The link to Voevodsky's webpage in README updated

The link to Voevodsky's webpage in README updated

Fix list

add link to hoq

update README

removed some examples (to be updated)

added some examples

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

Conflicts:
examples/univalence.ctt

minor changes

Update README

Add the proof of univalence using glue with isos

Fix imports

Fix typo in typechecker and redefine isoId using glue

Revert to using iso instead of equiv

Some lemmas about equivs

Update aim talk

Fixed lemCompInv

Equations for subst and J

Fix typo in inferType

Restate univalence

Update susp

Update README and update demo.ctt

Cleaning and reorganization of files

Merge branch 'no_regular' into equiv

# Conflicts:
# CTT.hs
# Eval.hs

Cleaning

Add typechecking for glueElem

Remove old code for eqToIso and gradLemma for isos

Make more names unqualified when importing Map and reorganization+cleaning

Improve printing of fst and snd

Remove commented code for GlueLine, GlueLineElem, CompElem and ElimComp

Reintroduce transport

Reintroduce glueElem

Finish the proof of univalence

Start adding gradlemma to finish proof of univalence

A proof of univalence (wip)

Adds projections for equivs

Typo

Don't require equivalences to be eta-expanded

Finished eqToEquiv

Fix handling of neutral for composition in sums

Fix hisos''

Fix printing

Convertability for HSum

Rename hiso to equiv

Equivalences instead of isos (wip)

Make bool, circle and integer compile

Add lemSimpl

Convertability for hComp

Update aim.ctt again

Update aim.ctt

Add AIM talk

Less definitional equalities for glue

Throw out transport

Merge branch 'hisoproj' into no_regular

Conflicts:
Eval.hs

Finished eqToIso and removed constants for comp in U

Update squeezeHIT

Equality to isomorphism (wip)

define trans in terms of gencomp

Added fill as a term and comp is now genComp

Add genComp and some examples for debugging

remove commented code

Adapted HITs

Fix for neutral unglues

Added neutral values for unglue

Adapted

Added constructor for comp in U

Fix use of compLine

Fix add_comm

isNeutralComp, small fixes to comp and comment things in bool

Adapted prelude

Finished first version

Adapted compGlue

Started adapting for the non-regular setting (wip)

Add direct proof that s2 is trivial (for the HIT definition of S2)

simple examples on nat and list

Isomorphism of the direct and the susp definition of S2

Fix the bug in transport and add optimizations to compElem and elimComp

Add exchange law and genPiS3

Change order in checkPathSystem

Add check that systems don't contain the same face multiple times in resolver

The loop space of the torus is equal to Z * Z

Cleaning

Clean helix

More efficient implementation of environments

Comment the two slowest tests in mystery

Add optimization to act

Add new proof that loopS1 is a set
Remove unnecessary imports