cubicaltt.git
9 years agoAdd the proof of univalence using glue with isos
Anders Mörtberg [Thu, 2 Jul 2015 07:18:40 +0000 (09:18 +0200)]
Add the proof of univalence using glue with isos

9 years agoFix imports
Anders Mörtberg [Wed, 1 Jul 2015 12:38:45 +0000 (14:38 +0200)]
Fix imports

9 years agoFix typo in typechecker and redefine isoId using glue
Anders Mörtberg [Tue, 30 Jun 2015 19:27:00 +0000 (21:27 +0200)]
Fix typo in typechecker and redefine isoId using glue

9 years agoRevert to using iso instead of equiv
Anders Mörtberg [Tue, 30 Jun 2015 11:09:18 +0000 (13:09 +0200)]
Revert to using iso instead of equiv

9 years agoSome lemmas about equivs
Anders [Mon, 29 Jun 2015 11:31:21 +0000 (13:31 +0200)]
Some lemmas about equivs

9 years agoUpdate aim talk
Anders [Mon, 29 Jun 2015 11:31:09 +0000 (13:31 +0200)]
Update aim talk

9 years agoFixed lemCompInv
Simon Huber [Sun, 28 Jun 2015 00:41:57 +0000 (02:41 +0200)]
Fixed lemCompInv

9 years agoEquations for subst and J
Simon Huber [Wed, 24 Jun 2015 09:50:42 +0000 (11:50 +0200)]
Equations for subst and J

9 years agoFix typo in inferType
Simon Huber [Mon, 22 Jun 2015 10:40:44 +0000 (12:40 +0200)]
Fix typo in inferType

9 years agoRestate univalence
Anders [Thu, 18 Jun 2015 16:57:12 +0000 (18:57 +0200)]
Restate univalence

9 years agoUpdate susp
Anders [Thu, 18 Jun 2015 16:53:12 +0000 (18:53 +0200)]
Update susp

9 years agoUpdate README and update demo.ctt
Anders [Thu, 18 Jun 2015 16:45:17 +0000 (18:45 +0200)]
Update README and update demo.ctt

9 years agoCleaning and reorganization of files
Anders [Thu, 18 Jun 2015 16:23:39 +0000 (18:23 +0200)]
Cleaning and reorganization of files

9 years agoMerge branch 'no_regular' into equiv
Anders [Thu, 18 Jun 2015 14:44:49 +0000 (16:44 +0200)]
Merge branch 'no_regular' into equiv

# Conflicts:
# CTT.hs
# Eval.hs

9 years agoCleaning
Anders [Thu, 18 Jun 2015 14:34:22 +0000 (16:34 +0200)]
Cleaning

9 years agoAdd typechecking for glueElem
Anders [Thu, 18 Jun 2015 14:26:42 +0000 (16:26 +0200)]
Add typechecking for glueElem

9 years agoRemove old code for eqToIso and gradLemma for isos
Anders [Thu, 18 Jun 2015 14:26:18 +0000 (16:26 +0200)]
Remove old code for eqToIso and gradLemma for isos

9 years agoMake more names unqualified when importing Map and reorganization+cleaning
Anders [Thu, 18 Jun 2015 14:25:59 +0000 (16:25 +0200)]
Make more names unqualified when importing Map and reorganization+cleaning

9 years agoImprove printing of fst and snd
Anders [Thu, 18 Jun 2015 13:53:22 +0000 (15:53 +0200)]
Improve printing of fst and snd

9 years agoRemove commented code for GlueLine, GlueLineElem, CompElem and ElimComp
Anders [Thu, 18 Jun 2015 13:52:59 +0000 (15:52 +0200)]
Remove commented code for GlueLine, GlueLineElem, CompElem and ElimComp

9 years agoReintroduce transport
Anders [Thu, 18 Jun 2015 13:37:17 +0000 (15:37 +0200)]
Reintroduce transport

9 years agoReintroduce glueElem
Anders [Thu, 18 Jun 2015 13:31:49 +0000 (15:31 +0200)]
Reintroduce glueElem

9 years agoFinish the proof of univalence
Anders [Wed, 17 Jun 2015 15:43:48 +0000 (17:43 +0200)]
Finish the proof of univalence

9 years agoStart adding gradlemma to finish proof of univalence
Anders Mörtberg [Wed, 17 Jun 2015 09:09:09 +0000 (11:09 +0200)]
Start adding gradlemma to finish proof of univalence

9 years agoA proof of univalence (wip)
Simon Huber [Tue, 16 Jun 2015 20:27:34 +0000 (22:27 +0200)]
A proof of univalence (wip)

9 years agoAdds projections for equivs
Simon Huber [Tue, 16 Jun 2015 20:11:52 +0000 (22:11 +0200)]
Adds projections for equivs

9 years agoTypo
Simon Huber [Tue, 16 Jun 2015 08:48:32 +0000 (10:48 +0200)]
Typo

9 years agoDon't require equivalences to be eta-expanded
Simon Huber [Tue, 16 Jun 2015 08:15:22 +0000 (10:15 +0200)]
Don't require equivalences to be eta-expanded

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

9 years agoFix handling of neutral for composition in sums
Simon Huber [Mon, 15 Jun 2015 09:15:58 +0000 (11:15 +0200)]
Fix handling of neutral for composition in sums

9 years agoFix hisos''
Anders [Sat, 13 Jun 2015 08:46:36 +0000 (10:46 +0200)]
Fix hisos''

9 years agoFix printing
Anders [Fri, 12 Jun 2015 10:45:41 +0000 (12:45 +0200)]
Fix printing

9 years agoConvertability for HSum
Simon Huber [Wed, 10 Jun 2015 09:21:36 +0000 (11:21 +0200)]
Convertability for HSum

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