cubicaltt.git
9 years agoFinished eqToEquiv
Simon Huber [Mon, 15 Jun 2015 12:51:25 +0000 (14:51 +0200)]
Finished eqToEquiv

9 years agoRename hiso to equiv
Simon Huber [Tue, 9 Jun 2015 13:48:42 +0000 (15:48 +0200)]
Rename hiso to equiv

9 years agoEquivalences instead of isos (wip)
Simon Huber [Tue, 9 Jun 2015 12:46:57 +0000 (14:46 +0200)]
Equivalences instead of isos (wip)

9 years agoMake bool, circle and integer compile
Anders [Mon, 8 Jun 2015 12:42:23 +0000 (14:42 +0200)]
Make bool, circle and integer compile

9 years agoAdd lemSimpl
Anders [Mon, 8 Jun 2015 12:26:44 +0000 (14:26 +0200)]
Add lemSimpl

9 years agoConvertability for hComp
Simon Huber [Mon, 8 Jun 2015 10:04:32 +0000 (12:04 +0200)]
Convertability for hComp

9 years agoUpdate aim.ctt again
Anders Mörtberg [Sat, 6 Jun 2015 09:23:12 +0000 (11:23 +0200)]
Update aim.ctt again

9 years agoUpdate aim.ctt
Anders Mörtberg [Sat, 6 Jun 2015 09:18:14 +0000 (11:18 +0200)]
Update aim.ctt

9 years agoAdd AIM talk
Anders Mörtberg [Sat, 6 Jun 2015 09:15:14 +0000 (11:15 +0200)]
Add AIM talk

9 years agoLess definitional equalities for glue
Simon Huber [Fri, 5 Jun 2015 15:54:27 +0000 (17:54 +0200)]
Less definitional equalities for glue

9 years agoThrow out transport
Simon Huber [Fri, 5 Jun 2015 14:18:22 +0000 (16:18 +0200)]
Throw out transport

9 years agoMerge branch 'hisoproj' into no_regular
Simon Huber [Fri, 5 Jun 2015 13:56:59 +0000 (15:56 +0200)]
Merge branch 'hisoproj' into no_regular

Conflicts:
Eval.hs

9 years agoFinished eqToIso and removed constants for comp in U
Simon Huber [Fri, 5 Jun 2015 13:50:26 +0000 (15:50 +0200)]
Finished eqToIso and removed constants for comp in U

9 years agoUpdate squeezeHIT
Anders Mörtberg [Thu, 4 Jun 2015 20:34:47 +0000 (22:34 +0200)]
Update squeezeHIT

9 years agoEquality to isomorphism (wip)
Simon Huber [Thu, 4 Jun 2015 19:52:36 +0000 (21:52 +0200)]
Equality to isomorphism (wip)

9 years agodefine trans in terms of gencomp
Anders Mörtberg [Thu, 4 Jun 2015 19:43:20 +0000 (21:43 +0200)]
define trans in terms of gencomp

9 years agoAdded fill as a term and comp is now genComp
Simon Huber [Thu, 4 Jun 2015 16:03:22 +0000 (18:03 +0200)]
Added fill as a term and comp is now genComp

9 years agoAdd genComp and some examples for debugging
Anders [Thu, 4 Jun 2015 13:15:37 +0000 (15:15 +0200)]
Add genComp and some examples for debugging

9 years agoremove commented code
Anders [Thu, 4 Jun 2015 12:47:21 +0000 (14:47 +0200)]
remove commented code

9 years agoAdapted HITs
Simon Huber [Thu, 4 Jun 2015 10:49:29 +0000 (12:49 +0200)]
Adapted HITs

9 years agoFix for neutral unglues
Simon Huber [Thu, 4 Jun 2015 09:06:40 +0000 (11:06 +0200)]
Fix for neutral unglues

9 years agoAdded neutral values for unglue
Simon Huber [Thu, 4 Jun 2015 08:35:41 +0000 (10:35 +0200)]
Added neutral values for unglue

9 years agoAdapted
Simon Huber [Thu, 4 Jun 2015 08:08:43 +0000 (10:08 +0200)]
Adapted

9 years agoAdded constructor for comp in U
Simon Huber [Thu, 4 Jun 2015 08:08:33 +0000 (10:08 +0200)]
Added constructor for comp in U

9 years agoFix use of compLine
Simon Huber [Wed, 3 Jun 2015 20:05:07 +0000 (22:05 +0200)]
Fix use of compLine

9 years agoFix add_comm
Anders Mörtberg [Wed, 3 Jun 2015 18:48:42 +0000 (20:48 +0200)]
Fix add_comm

9 years agoisNeutralComp, small fixes to comp and comment things in bool
Anders [Wed, 3 Jun 2015 15:16:08 +0000 (17:16 +0200)]
isNeutralComp, small fixes to comp and comment things in bool

9 years agoAdapted prelude
Simon Huber [Wed, 3 Jun 2015 14:06:03 +0000 (16:06 +0200)]
Adapted prelude

9 years agoFinished first version
Simon Huber [Wed, 3 Jun 2015 14:04:57 +0000 (16:04 +0200)]
Finished first version

9 years agoAdapted compGlue
Simon Huber [Wed, 3 Jun 2015 12:27:03 +0000 (14:27 +0200)]
Adapted compGlue

9 years agoStarted adapting for the non-regular setting (wip)
Simon Huber [Tue, 2 Jun 2015 13:03:56 +0000 (15:03 +0200)]
Started adapting for the non-regular setting (wip)

9 years agoAdd direct proof that s2 is trivial (for the HIT definition of S2)
Anders [Mon, 18 May 2015 09:29:02 +0000 (11:29 +0200)]
Add direct proof that s2 is trivial (for the HIT definition of S2)

9 years agosimple examples on nat and list
coquand [Sat, 16 May 2015 09:04:05 +0000 (11:04 +0200)]
simple examples on nat and list

9 years agoIsomorphism of the direct and the susp definition of S2
Anders [Tue, 12 May 2015 08:54:16 +0000 (10:54 +0200)]
Isomorphism of the direct and the susp definition of S2

9 years agoFix the bug in transport and add optimizations to compElem and elimComp
Anders [Mon, 11 May 2015 12:18:24 +0000 (14:18 +0200)]
Fix the bug in transport and add optimizations to compElem and elimComp

9 years agoAdd exchange law and genPiS3
Anders [Fri, 8 May 2015 13:29:25 +0000 (15:29 +0200)]
Add exchange law and genPiS3

9 years agoChange order in checkPathSystem
Anders [Fri, 8 May 2015 13:28:49 +0000 (15:28 +0200)]
Change order in checkPathSystem

9 years agoAdd check that systems don't contain the same face multiple times in resolver
Anders [Wed, 6 May 2015 17:13:01 +0000 (19:13 +0200)]
Add check that systems don't contain the same face multiple times in resolver

9 years agoThe loop space of the torus is equal to Z * Z
Anders [Wed, 6 May 2015 16:59:08 +0000 (18:59 +0200)]
The loop space of the torus is equal to Z * Z

9 years agoCleaning
Anders [Wed, 6 May 2015 11:57:06 +0000 (13:57 +0200)]
Cleaning

9 years agoClean helix
Anders [Wed, 6 May 2015 09:57:53 +0000 (11:57 +0200)]
Clean helix

9 years agoMore efficient implementation of environments
Anders [Wed, 6 May 2015 09:53:58 +0000 (11:53 +0200)]
More efficient implementation of environments

9 years agoComment the two slowest tests in mystery
Anders Mörtberg [Tue, 5 May 2015 20:30:28 +0000 (22:30 +0200)]
Comment the two slowest tests in mystery

9 years agoAdd optimization to act
Anders Mörtberg [Tue, 5 May 2015 20:30:17 +0000 (22:30 +0200)]
Add optimization to act

9 years agoAdd new proof that loopS1 is a set
Anders Mörtberg [Tue, 5 May 2015 18:54:03 +0000 (20:54 +0200)]
Add new proof that loopS1 is a set
Remove unnecessary imports

9 years agoMerge pull request #10 from dlicata335/master
mortberg [Tue, 5 May 2015 18:09:29 +0000 (20:09 +0200)]
Merge pull request #10 from dlicata335/master

cleaned up mystery.ctt

9 years agocleaned up mystery.ctt for inclusion in repository: move rest of Omega(S1) = Z to...
Dan Licata [Tue, 5 May 2015 15:42:15 +0000 (11:42 -0400)]
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

9 years agoSwap test2 and test3 to correspond to what is in cubical
Anders Mörtberg [Tue, 5 May 2015 00:43:47 +0000 (02:43 +0200)]
Swap test2 and test3 to correspond to what is in cubical

9 years agoAdd fix to comp for sums
Anders Mörtberg [Tue, 5 May 2015 00:10:41 +0000 (02:10 +0200)]
Add fix to comp for sums

9 years agoAdd pi4s3 until test0To5
Anders Mörtberg [Mon, 4 May 2015 23:55:45 +0000 (01:55 +0200)]
Add pi4s3 until test0To5

9 years agoAdd -t flag
Anders Mörtberg [Mon, 4 May 2015 23:55:08 +0000 (01:55 +0200)]
Add -t flag

9 years agonicer error msg
Simon Huber [Mon, 4 May 2015 10:32:18 +0000 (12:32 +0200)]
nicer error msg

9 years agofixed printing of glueLine
Simon Huber [Mon, 4 May 2015 10:04:17 +0000 (12:04 +0200)]
fixed printing of glueLine

9 years agomove neutrality test in app of a split to a composition
Simon Huber [Mon, 4 May 2015 09:27:37 +0000 (11:27 +0200)]
move neutrality test in app of a split to a composition

9 years agouse unqualified mapWithKey
Simon Huber [Thu, 30 Apr 2015 14:03:04 +0000 (16:03 +0200)]
use unqualified mapWithKey

9 years agoAdd missing spaces
Anders Mörtberg [Sun, 3 May 2015 16:18:08 +0000 (18:18 +0200)]
Add missing spaces

9 years agoMerge pull request #9 from dlicata335/master
mortberg [Sun, 3 May 2015 16:14:38 +0000 (18:14 +0200)]
Merge pull request #9 from dlicata335/master

torus =  S1 * S1 example

9 years agosix is not the successor of six
Dan Licata [Sat, 2 May 2015 18:06:23 +0000 (14:06 -0400)]
six is not the successor of six

9 years agomystery example: beta reduce some compIds
Dan Licata [Sat, 2 May 2015 15:18:07 +0000 (11:18 -0400)]
mystery example: beta reduce some compIds

9 years agocompile with -rtsopts so you can set the stack space
Dan Licata [Sat, 2 May 2015 14:45:59 +0000 (10:45 -0400)]
compile with -rtsopts so you can set the stack space

9 years agouse synthetic homotopy theory to get a function on numbers
Dan Licata [Sat, 2 May 2015 14:45:22 +0000 (10:45 -0400)]
use synthetic homotopy theory to get a function on numbers

9 years agouse synthetic homotopy theory to get a function on numbers
Dan Licata [Sat, 2 May 2015 14:45:09 +0000 (10:45 -0400)]
use synthetic homotopy theory to get a function on numbers

9 years agotorus = two circles proof cleanup
Dan Licata [Fri, 1 May 2015 17:36:42 +0000 (13:36 -0400)]
torus = two circles proof cleanup

9 years agotorus = two circles proof
Dan Licata [Fri, 1 May 2015 14:35:02 +0000 (10:35 -0400)]
torus = two circles proof

9 years agoadd more parentheses
Simon Huber [Thu, 30 Apr 2015 13:37:00 +0000 (15:37 +0200)]
add more parentheses

9 years agonon-trivial homotopy in the loop space of stwo
Simon Huber [Thu, 30 Apr 2015 13:32:40 +0000 (15:32 +0200)]
non-trivial homotopy in the loop space of stwo

9 years agoallow overshadowing of names
Simon Huber [Thu, 30 Apr 2015 13:32:12 +0000 (15:32 +0200)]
allow overshadowing of names

9 years agoupdated collection
coquand [Thu, 30 Apr 2015 12:01:17 +0000 (14:01 +0200)]
updated collection

9 years agoupdated setTrunc
coquand [Thu, 30 Apr 2015 12:00:22 +0000 (14:00 +0200)]
updated setTrunc

9 years agoadded some test for pi1S2
coquand [Thu, 30 Apr 2015 11:56:57 +0000 (13:56 +0200)]
added some test for pi1S2

9 years agopi1S2 is trivial
coquand [Thu, 30 Apr 2015 11:52:20 +0000 (13:52 +0200)]
pi1S2 is trivial

9 years agopiS2 is trivial
coquand [Thu, 30 Apr 2015 11:44:38 +0000 (13:44 +0200)]
piS2 is trivial

9 years agounivalence
coquand [Thu, 30 Apr 2015 10:23:58 +0000 (12:23 +0200)]
univalence

9 years agothe collection of sets is a groupoid
coquand [Thu, 30 Apr 2015 08:30:52 +0000 (10:30 +0200)]
the collection of sets is a groupoid

9 years agoadded glueLine (wip)
Simon Huber [Wed, 29 Apr 2015 14:16:03 +0000 (16:16 +0200)]
added glueLine (wip)

9 years agoimprove error message
Simon Huber [Wed, 29 Apr 2015 12:19:41 +0000 (14:19 +0200)]
improve error message

9 years agoadded hopf fibration
coquand [Wed, 29 Apr 2015 10:28:10 +0000 (12:28 +0200)]
added hopf fibration

9 years agomore efficient version of groupoid truncation
coquand [Wed, 29 Apr 2015 07:50:57 +0000 (09:50 +0200)]
more efficient version of groupoid truncation

9 years agonicer proof of lemtransport
coquand [Tue, 28 Apr 2015 17:59:04 +0000 (19:59 +0200)]
nicer proof of lemtransport

9 years agoan example of normal form
coquand [Tue, 28 Apr 2015 16:33:36 +0000 (18:33 +0200)]
an example of normal form

9 years agoadded groupoid truncation
coquand [Tue, 28 Apr 2015 11:37:09 +0000 (13:37 +0200)]
added groupoid truncation

9 years agoadded pi1s2
coquand [Tue, 28 Apr 2015 11:22:26 +0000 (13:22 +0200)]
added pi1s2

9 years agoclean mult
coquand [Mon, 27 Apr 2015 19:44:41 +0000 (21:44 +0200)]
clean mult

9 years agoadded some examples for pi1S2
coquand [Mon, 27 Apr 2015 19:42:32 +0000 (21:42 +0200)]
added some examples for pi1S2

9 years agoAdd the test of parsing output from integer back
Anders [Thu, 23 Apr 2015 15:36:31 +0000 (17:36 +0200)]
Add the test of parsing output from integer back

9 years agoFix set
Anders [Thu, 23 Apr 2015 15:26:25 +0000 (17:26 +0200)]
Fix set

9 years agoNormalize formulas
Anders [Thu, 23 Apr 2015 15:26:18 +0000 (17:26 +0200)]
Normalize formulas

9 years agoFix dnf
Anders [Thu, 23 Apr 2015 15:04:11 +0000 (17:04 +0200)]
Fix dnf

9 years agoElimination principle for set truncation
Anders [Thu, 23 Apr 2015 15:04:00 +0000 (17:04 +0200)]
Elimination principle for set truncation

9 years agobugix: take the border of the system where is=js
Simon Huber [Thu, 23 Apr 2015 12:57:28 +0000 (14:57 +0200)]
bugix: take the border of the system where is=js

9 years agoRefactoring of examples
Anders Mörtberg [Tue, 21 Apr 2015 18:19:11 +0000 (20:19 +0200)]
Refactoring of examples

9 years agoAdd normalization of environments
Anders [Tue, 21 Apr 2015 15:59:11 +0000 (17:59 +0200)]
Add normalization of environments

9 years agoproof that mult is an equivalence
coquand [Tue, 21 Apr 2015 15:18:03 +0000 (17:18 +0200)]
proof that mult is an equivalence

9 years agoproof that mult is an equivalence
coquand [Tue, 21 Apr 2015 15:16:20 +0000 (17:16 +0200)]
proof that mult is an equivalence

9 years agoupdated proofs of Hedberg's Theorem
coquand [Tue, 21 Apr 2015 14:57:12 +0000 (16:57 +0200)]
updated proofs of Hedberg's Theorem

9 years agoImprove printing of lambdas and paths
Anders [Tue, 21 Apr 2015 12:38:16 +0000 (14:38 +0200)]
Improve printing of lambdas and paths

9 years agoMake conversion use a list of names instead
Anders [Tue, 21 Apr 2015 10:10:33 +0000 (12:10 +0200)]
Make conversion use a list of names instead

9 years agoRemove unnecessary argument to addBranch
Anders [Tue, 21 Apr 2015 09:44:39 +0000 (11:44 +0200)]
Remove unnecessary argument to addBranch

9 years agoRemove unnecessary monadic code in Typechecker (no more localM!)
Anders [Tue, 21 Apr 2015 09:36:29 +0000 (11:36 +0200)]
Remove unnecessary monadic code in Typechecker (no more localM!)

9 years agoChange ? to !
Anders Mörtberg [Tue, 21 Apr 2015 08:11:02 +0000 (10:11 +0200)]
Change ? to !