coquand [Sat, 26 Dec 2015 16:14:38 +0000 (17:14 +0100)]
proof of univalence
Simon Huber [Thu, 17 Dec 2015 08:51:52 +0000 (09:51 +0100)]
Fixed eqToEquiv
Simon Huber [Wed, 16 Dec 2015 11:30:48 +0000 (12:30 +0100)]
Switched back to equiv, simplified glue
Simon Huber [Tue, 15 Dec 2015 13:53:36 +0000 (14:53 +0100)]
Bugfix for type checking glueElems by Fabian Ruch
Simon Huber [Mon, 14 Dec 2015 15:14:36 +0000 (16:14 +0100)]
Efficient @@ for fresh names
We don't have to call act if the name is fresh.
Simon Huber [Mon, 14 Dec 2015 14:37:23 +0000 (15:37 +0100)]
Simplified pathComp
Anders Mörtberg [Thu, 3 Dec 2015 14:30:41 +0000 (09:30 -0500)]
add a short version of setquot
Anders Mörtberg [Wed, 2 Dec 2015 22:30:50 +0000 (17:30 -0500)]
Prove direct version of uahp
Anders Mörtberg [Wed, 2 Dec 2015 20:00:54 +0000 (15:00 -0500)]
fix comment
Anders Mörtberg [Wed, 2 Dec 2015 19:57:00 +0000 (14:57 -0500)]
Cleaning
Anders Mörtberg [Wed, 2 Dec 2015 19:33:17 +0000 (14:33 -0500)]
finish setquot example
Anders Mörtberg [Wed, 2 Dec 2015 19:33:06 +0000 (14:33 -0500)]
prove that bool is a set
Anders Mörtberg [Wed, 2 Dec 2015 03:09:34 +0000 (22:09 -0500)]
prove that hProp is a set
Anders Mörtberg [Wed, 2 Dec 2015 01:56:38 +0000 (20:56 -0500)]
prove uahp
Anders Mörtberg [Tue, 1 Dec 2015 23:18:25 +0000 (18:18 -0500)]
setquot
Simon Huber [Fri, 11 Sep 2015 20:18:54 +0000 (22:18 +0200)]
Another formulation of univalence
Anders Mörtberg [Thu, 19 Nov 2015 15:40:50 +0000 (10:40 -0500)]
indentation
Anders Mörtberg [Thu, 19 Nov 2015 05:09:00 +0000 (00:09 -0500)]
Add a test that of a simple example where Coq gets stuck but cubicaltt don't
Anders Mörtberg [Mon, 26 Oct 2015 14:52:21 +0000 (10:52 -0400)]
Fix printing of Pi types
Anders Mörtberg [Mon, 26 Oct 2015 02:33:08 +0000 (22:33 -0400)]
Revert my previous changes to GNUMakefile and add -dep-suffix to the build-Makefile target
Anders Mörtberg [Mon, 26 Oct 2015 02:21:06 +0000 (22:21 -0400)]
Merge pull request #23 from DanGrayson/improve-Makefile
fix makefile for ghc 7.10
Daniel R. Grayson [Mon, 26 Oct 2015 02:14:20 +0000 (22:14 -0400)]
fix makefile for ghc 7.10
Anders Mörtberg [Mon, 26 Oct 2015 02:05:44 +0000 (22:05 -0400)]
Update README.md
Anders Mörtberg [Mon, 26 Oct 2015 02:02:42 +0000 (22:02 -0400)]
Update README.md
Anders Mörtberg [Sun, 25 Oct 2015 22:28:05 +0000 (18:28 -0400)]
Temporary fix to the Makefile
Anders Mörtberg [Sun, 25 Oct 2015 22:06:01 +0000 (18:06 -0400)]
Merge branch 'DanGrayson-improve-Makefile'
Anders Mörtberg [Sun, 25 Oct 2015 22:05:39 +0000 (18:05 -0400)]
Merge branch 'improve-Makefile' of https://github.com/DanGrayson/cubicaltt into DanGrayson-improve-Makefile
Conflicts:
README.md
Daniel R. Grayson [Fri, 23 Oct 2015 17:17:42 +0000 (13:17 -0400)]
add examples/Makefile for ctt tags files
Daniel R. Grayson [Fri, 23 Oct 2015 17:06:22 +0000 (13:06 -0400)]
remove INCLUDE option and add Makefile to repository
Daniel R. Grayson [Fri, 23 Oct 2015 16:15:05 +0000 (12:15 -0400)]
update Makefile
Daniel R. Grayson [Fri, 23 Oct 2015 15:05:54 +0000 (11:05 -0400)]
README...
Daniel R. Grayson [Thu, 22 Oct 2015 12:39:45 +0000 (08:39 -0400)]
improve Makefile
Daniel R. Grayson [Thu, 22 Oct 2015 11:52:51 +0000 (07:52 -0400)]
rename makefile
Anders Mörtberg [Wed, 21 Oct 2015 15:45:00 +0000 (11:45 -0400)]
Merge pull request #21 from tulcod/master
Update README.md: how to build with cabal
Auke Booij [Tue, 20 Oct 2015 18:07:45 +0000 (19:07 +0100)]
Update README.md: how to build with cabal
Daniel R. Grayson [Mon, 19 Oct 2015 20:17:45 +0000 (16:17 -0400)]
update README
Daniel R. Grayson [Mon, 19 Oct 2015 20:15:49 +0000 (16:15 -0400)]
update README
Daniel R. Grayson [Mon, 19 Oct 2015 20:13:13 +0000 (16:13 -0400)]
add "make TAGS" command, using hasktags
Daniel R. Grayson [Mon, 19 Oct 2015 20:08:54 +0000 (16:08 -0400)]
Merge branch 'master' of github.com:mortberg/cubicaltt into improve-Makefile
Anders Mörtberg [Fri, 16 Oct 2015 15:51:13 +0000 (11:51 -0400)]
Remove some old tests
Anders Mörtberg [Fri, 16 Oct 2015 15:47:20 +0000 (11:47 -0400)]
Patch and clean the torus example
Daniel R. Grayson [Thu, 15 Oct 2015 14:21:43 +0000 (10:21 -0400)]
improve Makefile
Anders Mörtberg [Wed, 14 Oct 2015 21:31:36 +0000 (17:31 -0400)]
Update cabal file (fix typo, remove old email address and experiments/*ctt)
Anders Mörtberg [Wed, 14 Oct 2015 21:22:34 +0000 (17:22 -0400)]
Merge pull request #19 from tulcod/haskell2010
Move to Haskell2010
Anders Mörtberg [Wed, 14 Oct 2015 19:51:12 +0000 (15:51 -0400)]
Merge pull request #18 from tulcod/master
Converted the project into a cabal project
Auke Booij [Wed, 14 Oct 2015 13:18:01 +0000 (14:18 +0100)]
Move to haskell 2010
Auke Booij [Wed, 14 Oct 2015 13:08:55 +0000 (14:08 +0100)]
Populate extra-source-files
Auke Booij [Wed, 14 Oct 2015 13:02:30 +0000 (14:02 +0100)]
Complete cubicaltt.cabal: list all generated modules, improve syntax.
Auke Booij [Wed, 14 Oct 2015 12:32:45 +0000 (13:32 +0100)]
Rename executable to cubical (as in Makefile)
Auke Booij [Wed, 14 Oct 2015 09:14:20 +0000 (10:14 +0100)]
Converted the project into a cabal project.
Using the cabal project files, one can easily build this project in sandboxes.
It is also more easy to package for distribution.
Also includes a minor LICENSE file reformatting and encoding fix.
Original Makefile is still in place.
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''
projects / cubicaltt.git / log