bugix: take the border of the system where is=js

Refactoring of examples

Add normalization of environments

proof that mult is an equivalence

proof that mult is an equivalence

updated proofs of Hedberg's Theorem

Improve printing of lambdas and paths

Make conversion use a list of names instead

Remove unnecessary argument to addBranch

Remove unnecessary monadic code in Typechecker (no more localM!)

Change ? to !

Fix examples

Update graph script

Add testall

Fix helix

Fix newhedberg

Use old gensym and fresh again

Fix printing of VPi

Fix retract

Make normal print nicer names

Fix printing of @

Add quotient example

Split higherhit into multiple files

Merge remote-tracking branch 'origin/higherhits'

Fix the way @ binds (it is now like normal application)

Fix a TODO in the resolver (the arguments in a path constructors cannot refer to the path constructor itself)

Fix all the old examples of HITs

Remove the @ in PLabel

any isomorphism is an equivalence

if A and B are isomorphic, set A -> set B, normal form

if A and B are isomorphic, prop A -> prop B, normal form

result on equivalence of fibers

new proof of Hedberg's theorem

some examples

lookName error msg for debugging

bugfix in PBranches

let the system in a pcon know about all pcons in the sum

TODO: the current pcon should not know about itself

bugfix

bugfix in resolver

wip (not working yet)

Fix printing of goals and environments (TODO: Fix "susp (bool)"...)

Rewrite app and support using case-of

Use Except instead or Error

Remove tabs

Only show second part of VPi x (VLam ...)

Also normalize the type of lambdas and print VPi nicer

Use showTer1 to print closures

Fix uafunext2

Remove some incidentally commited holes

Reintroduce _ in identifier again

reintroduce nicer mkVar

keep name if we have it when generating a fresh name

change mkVar back to how it was

Add indentation to Checking and start changing mkVar (not working as expected wrt holes)

Only print File loaded if file type checks

Change gensym

Make holes print the context

Trailing whitespace

Fix undefined

Finish example of integers as a HIT

Remove some code from ex1

Fix bug in type checker for HITs

Fix undefined

Remove VUndef

Add very simple support for holes

Make list compile

Make undefined only occur as a declaration so that the type can be inferred

Undef is neutral (but there is an issue with inferType for undef)

Start defining integers as a HIT and proving that they are a set

Fix printing of fst, snd and lambdas

Update the description in demo.ctt

added some lines in ex1.ctt

added some lines in ex1.ctt

small change in helix.ctt

one example with constant functions

Fix bug in Resolver

Remove contr from equiv

license should include names

small modification in the file susp

Update help message

Update README

Move stream to experiments

Add dependency graph script

Update README

Lots of cleaning in the examples

Add equiv and uafunext2

Reorganized and cleaned some examples

Update README

Fix README

Update README

Update the README and examples

demo from the proglog talk

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.