use smart fst/snd in act

added thierrys examples (funext from univalence,helix)

fixing use of isNeutral

Fix parsing of trans, comp, etc.

Explicitly pass around the history

Merge pull request #6 from nad/master

Proved (?) that equality coincides with bisimilarity.

Start the proof that ua implies funext

Proved (?) that equality coincides with bisimilarity.

With help from Thierry Coquand and Simon Huber.

Clean examples

Add normalization function

funext from interval

don't crash the main loop if error in eval

split annotation is now the type not the family; typo in eval fixed

evaluate undefined into a closure

function should be known in def (for general recursion)

Cleaning

added thierrys adapted files

improve show of a sum

analogous fix for pathUniv

bugfix in pathUnivTrans

reintroduce faceEnv

Cleaned and simplified type checker

bugfix in simplify, conv; extended prelude

Fix parsing of /\

Fix error message when path constructors are written without the type in
curly braces

Cleaning

Update Makefile

readme

fix readme

fix readme

Update readme

Examples

app for VCompElem and VElimComp

Fix conversion of formulas

Fix isNeutral

Add more tests

Fix a bug in eqLemma

Add the circle (there is a bug)

Finish adding HITs

Add squeeze, fix some bugs and optimize(?) transport

moved transGlue; typo in compGlue

Add HITs (parsing and resolver missing)

examples

bugfix in trans

bugfix for act on a path

added compElem and elimComp (still buggy)

pairs now associate to the right

lemTest not in prelude..

added simplify for Trans and Comp

removed Map. here and there

fixed bug; switched a with b in hiso

enhanced and renamed emacs mode

Finish adding glue

Add evaluation of Glue and GlueElem

fixed compLine; improved error msg for @@

dont crash the resolver if expression could not be resolved

Update .gitignore

Fix printing of formulas in AppFormula

Add support for multiple bindings of dimensions

Fix printing of systems

Fix bug in gensym and add Square

Finish implementing comp

Parsing of systems

Started adding comp

the endpoints of a path should match the Id arguments; inferType

throw out Binder

time to wake up

reintroduced Convertible typeclass; fixed conv for formulas

fixed support for Env

Start adding inferType

Add 0 and 1 to parser and resolver

Use checkPath when checking IdP

Add .gitignore

Names are now strings

Add J

Fix a typo in the parser

added transport

show transport like we parse it; whitespace

added app of a formula

Add Id, Path, AppFormula and Trans.

funExt is working!

Add Connections

Rename to cubical

Start adding Id types

Remove Neutral data type

Clean Resolver

Start working on cubical type theory

Initial commit

Initial commit