simpler version of idToId in testEquiv

alternative definition of equivalences

start working on hz

Clean setquot

add IdPathTest1

minor modification to foo

another small test

change es' to es, not sure if this is correct...

Simpler version of gradlemmaU

minor changes

Add the missing line in comp!

another example

remove reglarity

add a shrink function that can be used to not print all of the output

Add VCompU to normal and conv

Add some test of normal forms

Reintroduce compU

add a short version of setquot

Prove direct version of uahp

fix comment

Cleaning

finish setquot example

prove that bool is a set

prove that hProp is a set

prove uahp

setquot

Another formulation of univalence

indentation

Add a test that of a simple example where Coq gets stuck but cubicaltt don't

Fix printing of Pi types

Revert my previous changes to GNUMakefile and add -dep-suffix to the build-Makefile target

Merge pull request #23 from DanGrayson/improve-Makefile

fix makefile for ghc 7.10

fix makefile for ghc 7.10

Update README.md

Update README.md

Temporary fix to the Makefile

Merge branch 'DanGrayson-improve-Makefile'

Merge branch 'improve-Makefile' of https://github.com/DanGrayson/cubicaltt into DanGrayson-improve-Makefile

Conflicts:
README.md

add examples/Makefile for ctt tags files

remove INCLUDE option and add Makefile to repository

update Makefile

README...

improve Makefile

rename makefile

Merge pull request #21 from tulcod/master

Update README.md: how to build with cabal

Update README.md: how to build with cabal

update README

update README

add "make TAGS" command, using hasktags

Merge branch 'master' of github.com:mortberg/cubicaltt into improve-Makefile

Remove some old tests

Patch and clean the torus example

improve Makefile

Update cabal file (fix typo, remove old email address and experiments/*ctt)

Merge pull request #19 from tulcod/haskell2010

Move to Haskell2010

Merge pull request #18 from tulcod/master

Converted the project into a cabal project

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.

improve Makefile

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