Daniel R. Grayson [Thu, 15 Oct 2015 14:21:43 +0000 (10:21 -0400)]
improve Makefile
Daniel R. Grayson [Sun, 11 Oct 2015 14:33:38 +0000 (10:33 -0400)]
improve Makefile
Anders Mörtberg [Mon, 5 Oct 2015 01:30:07 +0000 (21:30 -0400)]
Reintroduce hdata
Simon Huber [Thu, 17 Sep 2015 14:05:33 +0000 (16:05 +0200)]
Removed unGlue
Simon Huber [Thu, 10 Sep 2015 12:42:46 +0000 (14:42 +0200)]
Merge branch 'mutual'
Simon Huber [Thu, 10 Sep 2015 12:40:47 +0000 (14:40 +0200)]
Rename Simple into NonMutual and added sanity check
coquand [Tue, 8 Sep 2015 09:42:07 +0000 (11:42 +0200)]
updated README
Simon Huber [Mon, 31 Aug 2015 14:41:58 +0000 (16:41 +0200)]
Fixed and added comment for transpHIT
Simon Huber [Wed, 12 Aug 2015 15:31:28 +0000 (17:31 +0200)]
Reintroduced mutual (wip)
Simon Huber [Tue, 11 Aug 2015 11:36:10 +0000 (13:36 +0200)]
Fix squeezes
mortberg [Tue, 4 Aug 2015 06:11:20 +0000 (08:11 +0200)]
Merge pull request #14 from vladimirias/master
The link to Voevodsky's webpage in README updated
Vladimir Voevodsky [Sun, 2 Aug 2015 18:10:26 +0000 (01:10 +0700)]
The link to Voevodsky's webpage in README updated
Anders Mörtberg [Tue, 14 Jul 2015 15:56:16 +0000 (17:56 +0200)]
Fix list
Anders Mörtberg [Tue, 14 Jul 2015 15:55:29 +0000 (17:55 +0200)]
add link to hoq
coquand [Fri, 3 Jul 2015 11:30:17 +0000 (13:30 +0200)]
update README
coquand [Fri, 3 Jul 2015 11:28:57 +0000 (13:28 +0200)]
removed some examples (to be updated)
coquand [Fri, 3 Jul 2015 11:17:10 +0000 (13:17 +0200)]
added some examples
coquand [Fri, 3 Jul 2015 11:16:12 +0000 (13:16 +0200)]
Merge branch 'master' of https://github.com/mortberg/cubicaltt
Conflicts:
examples/univalence.ctt
coquand [Fri, 3 Jul 2015 11:15:06 +0000 (13:15 +0200)]
minor changes
Anders Mörtberg [Fri, 3 Jul 2015 08:02:49 +0000 (10:02 +0200)]
Update README
Anders Mörtberg [Thu, 2 Jul 2015 07:18:40 +0000 (09:18 +0200)]
Add the proof of univalence using glue with isos
Anders Mörtberg [Wed, 1 Jul 2015 12:38:45 +0000 (14:38 +0200)]
Fix imports
Anders Mörtberg [Tue, 30 Jun 2015 19:27:00 +0000 (21:27 +0200)]
Fix typo in typechecker and redefine isoId using glue
Anders Mörtberg [Tue, 30 Jun 2015 11:09:18 +0000 (13:09 +0200)]
Revert to using iso instead of equiv
Anders [Mon, 29 Jun 2015 11:31:21 +0000 (13:31 +0200)]
Some lemmas about equivs
Anders [Mon, 29 Jun 2015 11:31:09 +0000 (13:31 +0200)]
Update aim talk
Simon Huber [Sun, 28 Jun 2015 00:41:57 +0000 (02:41 +0200)]
Fixed lemCompInv
Simon Huber [Wed, 24 Jun 2015 09:50:42 +0000 (11:50 +0200)]
Equations for subst and J
Simon Huber [Mon, 22 Jun 2015 10:40:44 +0000 (12:40 +0200)]
Fix typo in inferType
Anders [Thu, 18 Jun 2015 16:57:12 +0000 (18:57 +0200)]
Restate univalence
Anders [Thu, 18 Jun 2015 16:53:12 +0000 (18:53 +0200)]
Update susp
Anders [Thu, 18 Jun 2015 16:45:17 +0000 (18:45 +0200)]
Update README and update demo.ctt
Anders [Thu, 18 Jun 2015 16:23:39 +0000 (18:23 +0200)]
Cleaning and reorganization of files
Anders [Thu, 18 Jun 2015 14:44:49 +0000 (16:44 +0200)]
Merge branch 'no_regular' into equiv
# Conflicts:
# CTT.hs
# Eval.hs
Anders [Thu, 18 Jun 2015 14:34:22 +0000 (16:34 +0200)]
Cleaning
Anders [Thu, 18 Jun 2015 14:26:42 +0000 (16:26 +0200)]
Add typechecking for glueElem
Anders [Thu, 18 Jun 2015 14:26:18 +0000 (16:26 +0200)]
Remove old code for eqToIso and gradLemma for isos
Anders [Thu, 18 Jun 2015 14:25:59 +0000 (16:25 +0200)]
Make more names unqualified when importing Map and reorganization+cleaning
Anders [Thu, 18 Jun 2015 13:53:22 +0000 (15:53 +0200)]
Improve printing of fst and snd
Anders [Thu, 18 Jun 2015 13:52:59 +0000 (15:52 +0200)]
Remove commented code for GlueLine, GlueLineElem, CompElem and ElimComp
Anders [Thu, 18 Jun 2015 13:37:17 +0000 (15:37 +0200)]
Reintroduce transport
Anders [Thu, 18 Jun 2015 13:31:49 +0000 (15:31 +0200)]
Reintroduce glueElem
Anders [Wed, 17 Jun 2015 15:43:48 +0000 (17:43 +0200)]
Finish the 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
Simon Huber [Tue, 16 Jun 2015 20:27:34 +0000 (22:27 +0200)]
A proof of univalence (wip)
Simon Huber [Tue, 16 Jun 2015 20:11:52 +0000 (22:11 +0200)]
Adds projections for equivs
Simon Huber [Tue, 16 Jun 2015 08:48:32 +0000 (10:48 +0200)]
Typo
Simon Huber [Tue, 16 Jun 2015 08:15:22 +0000 (10:15 +0200)]
Don't require equivalences to be eta-expanded
Simon Huber [Mon, 15 Jun 2015 12:51:25 +0000 (14:51 +0200)]
Finished eqToEquiv
Simon Huber [Mon, 15 Jun 2015 09:15:58 +0000 (11:15 +0200)]
Fix handling of neutral for composition in sums
Anders [Sat, 13 Jun 2015 08:46:36 +0000 (10:46 +0200)]
Fix hisos''
Anders [Fri, 12 Jun 2015 10:45:41 +0000 (12:45 +0200)]
Fix printing
Simon Huber [Wed, 10 Jun 2015 09:21:36 +0000 (11:21 +0200)]
Convertability for HSum
Simon Huber [Tue, 9 Jun 2015 13:48:42 +0000 (15:48 +0200)]
Rename hiso to equiv
Simon Huber [Tue, 9 Jun 2015 12:46:57 +0000 (14:46 +0200)]
Equivalences instead of isos (wip)
Anders [Mon, 8 Jun 2015 12:42:23 +0000 (14:42 +0200)]
Make bool, circle and integer compile
Anders [Mon, 8 Jun 2015 12:26:44 +0000 (14:26 +0200)]
Add lemSimpl
Simon Huber [Mon, 8 Jun 2015 10:04:32 +0000 (12:04 +0200)]
Convertability for hComp
Anders Mörtberg [Sat, 6 Jun 2015 09:23:12 +0000 (11:23 +0200)]
Update aim.ctt again
Anders Mörtberg [Sat, 6 Jun 2015 09:18:14 +0000 (11:18 +0200)]
Update aim.ctt
Anders Mörtberg [Sat, 6 Jun 2015 09:15:14 +0000 (11:15 +0200)]
Add AIM talk
Simon Huber [Fri, 5 Jun 2015 15:54:27 +0000 (17:54 +0200)]
Less definitional equalities for glue
Simon Huber [Fri, 5 Jun 2015 14:18:22 +0000 (16:18 +0200)]
Throw out transport
Simon Huber [Fri, 5 Jun 2015 13:56:59 +0000 (15:56 +0200)]
Merge branch 'hisoproj' into no_regular
Conflicts:
Eval.hs
Simon Huber [Fri, 5 Jun 2015 13:50:26 +0000 (15:50 +0200)]
Finished eqToIso and removed constants for comp in U
Anders Mörtberg [Thu, 4 Jun 2015 20:34:47 +0000 (22:34 +0200)]
Update squeezeHIT
Simon Huber [Thu, 4 Jun 2015 19:52:36 +0000 (21:52 +0200)]
Equality to isomorphism (wip)
Anders Mörtberg [Thu, 4 Jun 2015 19:43:20 +0000 (21:43 +0200)]
define trans in terms of gencomp
Simon Huber [Thu, 4 Jun 2015 16:03:22 +0000 (18:03 +0200)]
Added fill as a term and comp is now genComp
Anders [Thu, 4 Jun 2015 13:15:37 +0000 (15:15 +0200)]
Add genComp and some examples for debugging
Anders [Thu, 4 Jun 2015 12:47:21 +0000 (14:47 +0200)]
remove commented code
Simon Huber [Thu, 4 Jun 2015 10:49:29 +0000 (12:49 +0200)]
Adapted HITs
Simon Huber [Thu, 4 Jun 2015 09:06:40 +0000 (11:06 +0200)]
Fix for neutral unglues
Simon Huber [Thu, 4 Jun 2015 08:35:41 +0000 (10:35 +0200)]
Added neutral values for unglue
Simon Huber [Thu, 4 Jun 2015 08:08:43 +0000 (10:08 +0200)]
Adapted
Simon Huber [Thu, 4 Jun 2015 08:08:33 +0000 (10:08 +0200)]
Added constructor for comp in U
Simon Huber [Wed, 3 Jun 2015 20:05:07 +0000 (22:05 +0200)]
Fix use of compLine
Anders Mörtberg [Wed, 3 Jun 2015 18:48:42 +0000 (20:48 +0200)]
Fix add_comm
Anders [Wed, 3 Jun 2015 15:16:08 +0000 (17:16 +0200)]
isNeutralComp, small fixes to comp and comment things in bool
Simon Huber [Wed, 3 Jun 2015 14:06:03 +0000 (16:06 +0200)]
Adapted prelude
Simon Huber [Wed, 3 Jun 2015 14:04:57 +0000 (16:04 +0200)]
Finished first version
Simon Huber [Wed, 3 Jun 2015 12:27:03 +0000 (14:27 +0200)]
Adapted compGlue
Simon Huber [Tue, 2 Jun 2015 13:03:56 +0000 (15:03 +0200)]
Started adapting for the non-regular setting (wip)
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)
coquand [Sat, 16 May 2015 09:04:05 +0000 (11:04 +0200)]
simple examples on nat and list
Anders [Tue, 12 May 2015 08:54:16 +0000 (10:54 +0200)]
Isomorphism of the direct and the susp definition of S2
Anders [Mon, 11 May 2015 12:18:24 +0000 (14:18 +0200)]
Fix the bug in transport and add optimizations to compElem and elimComp
Anders [Fri, 8 May 2015 13:29:25 +0000 (15:29 +0200)]
Add exchange law and genPiS3
Anders [Fri, 8 May 2015 13:28:49 +0000 (15:28 +0200)]
Change order in checkPathSystem
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
Anders [Wed, 6 May 2015 16:59:08 +0000 (18:59 +0200)]
The loop space of the torus is equal to Z * Z
Anders [Wed, 6 May 2015 11:57:06 +0000 (13:57 +0200)]
Cleaning
Anders [Wed, 6 May 2015 09:57:53 +0000 (11:57 +0200)]
Clean helix
Anders [Wed, 6 May 2015 09:53:58 +0000 (11:53 +0200)]
More efficient implementation of environments
Anders Mörtberg [Tue, 5 May 2015 20:30:28 +0000 (22:30 +0200)]
Comment the two slowest tests in mystery
Anders Mörtberg [Tue, 5 May 2015 20:30:17 +0000 (22:30 +0200)]
Add optimization to act
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
mortberg [Tue, 5 May 2015 18:09:29 +0000 (20:09 +0200)]
Merge pull request #10 from dlicata335/master
cleaned up mystery.ctt
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
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
projects / cubicaltt.git / log