change printing of compU

added an example with ordinals

More cleaning

Add bool example to univalence.ctt

Cleaning and removal of duplicate code. Put all proofs of univalence in the same file

Refactoring and move old code on equivalences to experiments folder

Make aim.ctt compile

Merge branch 'compU'

# Conflicts:
# CTT.hs
# Eval.hs
# examples/testEquiv.ctt

Merge branch 'testUniv'

# Conflicts:
# examples/testContr.ctt
# examples/testEquiv.ctt

update aim.ctt

add standard formulation of univalence

an example of normal form

updated collection

small change

updated sigma, not use of J

updated multS1

circle now works with this version of univalence

changed compU

simple tests for univalence

neutral for compU

Makefile

other proof of univalence

corrected Eval

an example where we type-checked a normal form

proof of univalence?

univalence

proof of univalence

updated testContr

some lemmas about contractible types

testEquiv

simplified transIdFun

simpler version of idToId in testEquiv

testEquiv

simplified transIdFun

simpler version of idToId in testEquiv

alternative definition of equivalences

Fixed eqToEquiv

Switched back to equiv, simplified glue

Bugfix for type checking glueElems by Fabian Ruch

Efficient @@ for fresh names

We don't have to call act if the name is fresh.

Simplified pathComp

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.