Don't require equivalences to be eta-expanded

Finished eqToEquiv

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

Merge pull request #10 from dlicata335/master

cleaned up mystery.ctt

cleaned up mystery.ctt for inclusion in repository: move rest of Omega(S1) = Z to helix.ctt and import T = S1*S1 from torus.ctt

Swap test2 and test3 to correspond to what is in cubical

Add fix to comp for sums

Add pi4s3 until test0To5

Add -t flag

nicer error msg

fixed printing of glueLine

move neutrality test in app of a split to a composition

use unqualified mapWithKey

Add missing spaces

Merge pull request #9 from dlicata335/master

torus =  S1 * S1 example

six is not the successor of six

mystery example: beta reduce some compIds

compile with -rtsopts so you can set the stack space

use synthetic homotopy theory to get a function on numbers

use synthetic homotopy theory to get a function on numbers

torus = two circles proof cleanup

torus = two circles proof

add more parentheses

non-trivial homotopy in the loop space of stwo

allow overshadowing of names

updated collection

updated setTrunc

added some test for pi1S2

pi1S2 is trivial

piS2 is trivial

univalence

the collection of sets is a groupoid

added glueLine (wip)

improve error message

added hopf fibration

more efficient version of groupoid truncation

nicer proof of lemtransport

an example of normal form

added groupoid truncation

added pi1s2

clean mult

added some examples for pi1S2

Add the test of parsing output from integer back

Fix set

Normalize formulas

Fix dnf

Elimination principle for set truncation

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!)