Anders Mörtberg [Thu, 14 Jan 2016 14:59:51 +0000 (09:59 -0500)]
make bool compile and move tests using univalence for bool
Simon Huber [Thu, 14 Jan 2016 14:19:03 +0000 (15:19 +0100)]
Bugfix in compU and compGlue
Simon Huber [Tue, 12 Jan 2016 11:08:23 +0000 (12:08 +0100)]
Bugfix by Fabian Ruch
Anders Mörtberg [Sat, 9 Jan 2016 11:50:12 +0000 (12:50 +0100)]
fix bug
Anders Mörtberg [Fri, 8 Jan 2016 09:54:54 +0000 (10:54 +0100)]
cleaning
Anders Mörtberg [Thu, 7 Jan 2016 17:05:29 +0000 (18:05 +0100)]
comment gradLemmaU
Anders Mörtberg [Thu, 7 Jan 2016 17:05:22 +0000 (18:05 +0100)]
remove @@@
Anders Mörtberg [Thu, 7 Jan 2016 17:03:01 +0000 (18:03 +0100)]
dont write to a file
Anders Mörtberg [Thu, 7 Jan 2016 17:02:27 +0000 (18:02 +0100)]
"_" in constPath again
Anders Mörtberg [Tue, 5 Jan 2016 11:50:54 +0000 (12:50 +0100)]
use compConstLine
Anders Mörtberg [Tue, 5 Jan 2016 11:20:11 +0000 (12:20 +0100)]
add the huge normal form of corrUniv which trigger the bug
Anders Mörtberg [Tue, 5 Jan 2016 11:19:45 +0000 (12:19 +0100)]
remove a space in a comment
Anders Mörtberg [Tue, 5 Jan 2016 11:07:56 +0000 (12:07 +0100)]
change constPath to avoid strange bug
Anders Mörtberg [Tue, 5 Jan 2016 11:07:45 +0000 (12:07 +0100)]
comment
Anders Mörtberg [Tue, 5 Jan 2016 11:07:39 +0000 (12:07 +0100)]
add parsing of ! in beginning of idents
Anders Mörtberg [Tue, 5 Jan 2016 09:21:54 +0000 (10:21 +0100)]
remove all <_>
Anders Mörtberg [Tue, 5 Jan 2016 09:21:22 +0000 (10:21 +0100)]
change printing of compU
coquand [Mon, 4 Jan 2016 16:58:17 +0000 (17:58 +0100)]
added an example with ordinals
Anders Mörtberg [Mon, 4 Jan 2016 19:03:31 +0000 (20:03 +0100)]
More cleaning
Anders Mörtberg [Mon, 4 Jan 2016 18:47:44 +0000 (19:47 +0100)]
Add bool example to univalence.ctt
Anders Mörtberg [Mon, 4 Jan 2016 18:44:13 +0000 (19:44 +0100)]
Cleaning and removal of duplicate code. Put all proofs of univalence in the same file
Anders Mörtberg [Mon, 4 Jan 2016 18:18:40 +0000 (19:18 +0100)]
Refactoring and move old code on equivalences to experiments folder
Anders Mörtberg [Thu, 31 Dec 2015 08:03:46 +0000 (09:03 +0100)]
Make aim.ctt compile
Anders Mörtberg [Thu, 31 Dec 2015 07:54:15 +0000 (08:54 +0100)]
Merge branch 'compU'
# Conflicts:
# CTT.hs
# Eval.hs
# examples/testEquiv.ctt
Anders Mörtberg [Thu, 31 Dec 2015 07:24:29 +0000 (08:24 +0100)]
Merge branch 'testUniv'
# Conflicts:
# examples/testContr.ctt
# examples/testEquiv.ctt
Anders Mörtberg [Thu, 31 Dec 2015 07:15:53 +0000 (08:15 +0100)]
update aim.ctt
Anders Mörtberg [Wed, 30 Dec 2015 18:58:37 +0000 (19:58 +0100)]
add standard formulation of univalence
coquand [Wed, 30 Dec 2015 10:13:46 +0000 (11:13 +0100)]
an example of normal form
coquand [Tue, 29 Dec 2015 15:16:37 +0000 (16:16 +0100)]
updated collection
coquand [Tue, 29 Dec 2015 15:04:44 +0000 (16:04 +0100)]
small change
coquand [Tue, 29 Dec 2015 15:03:42 +0000 (16:03 +0100)]
updated sigma, not use of J
coquand [Tue, 29 Dec 2015 14:52:35 +0000 (15:52 +0100)]
updated multS1
coquand [Tue, 29 Dec 2015 11:42:12 +0000 (12:42 +0100)]
circle now works with this version of univalence
coquand [Sun, 27 Dec 2015 18:33:04 +0000 (19:33 +0100)]
changed compU
coquand [Sun, 27 Dec 2015 09:09:05 +0000 (10:09 +0100)]
simple tests for univalence
coquand [Sun, 27 Dec 2015 08:59:19 +0000 (09:59 +0100)]
neutral for compU
coquand [Sat, 26 Dec 2015 19:49:27 +0000 (20:49 +0100)]
Makefile
coquand [Sat, 26 Dec 2015 19:45:35 +0000 (20:45 +0100)]
other proof of univalence
coquand [Sat, 26 Dec 2015 19:22:53 +0000 (20:22 +0100)]
corrected Eval
coquand [Sat, 26 Dec 2015 19:02:12 +0000 (20:02 +0100)]
an example where we type-checked a normal form
coquand [Sat, 26 Dec 2015 17:27:18 +0000 (18:27 +0100)]
proof of univalence?
coquand [Sat, 26 Dec 2015 16:35:18 +0000 (17:35 +0100)]
univalence
coquand [Sat, 26 Dec 2015 16:14:38 +0000 (17:14 +0100)]
proof of univalence
coquand [Sat, 26 Dec 2015 12:26:42 +0000 (13:26 +0100)]
updated testContr
coquand [Tue, 22 Dec 2015 13:52:11 +0000 (14:52 +0100)]
some lemmas about contractible types
coquand [Sat, 19 Dec 2015 18:25:41 +0000 (19:25 +0100)]
testEquiv
coquand [Sat, 19 Dec 2015 18:04:59 +0000 (19:04 +0100)]
simplified transIdFun
coquand [Fri, 18 Dec 2015 20:42:17 +0000 (21:42 +0100)]
simpler version of idToId in testEquiv
coquand [Sat, 19 Dec 2015 18:25:41 +0000 (19:25 +0100)]
testEquiv
coquand [Sat, 19 Dec 2015 18:04:59 +0000 (19:04 +0100)]
simplified transIdFun
coquand [Fri, 18 Dec 2015 20:42:17 +0000 (21:42 +0100)]
simpler version of idToId in testEquiv
Anders Mörtberg [Fri, 18 Dec 2015 14:08:27 +0000 (09:08 -0500)]
alternative definition of equivalences
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 [Fri, 11 Dec 2015 21:39:35 +0000 (16:39 -0500)]
start working on hz
Anders Mörtberg [Fri, 11 Dec 2015 21:14:57 +0000 (16:14 -0500)]
Clean setquot
Anders Mörtberg [Wed, 9 Dec 2015 19:15:03 +0000 (14:15 -0500)]
add IdPathTest1
Anders Mörtberg [Fri, 4 Dec 2015 23:05:59 +0000 (18:05 -0500)]
minor modification to foo
Anders Mörtberg [Fri, 4 Dec 2015 20:07:10 +0000 (15:07 -0500)]
another small test
Anders Mörtberg [Fri, 4 Dec 2015 19:51:26 +0000 (14:51 -0500)]
change es' to es, not sure if this is correct...
Anders Mörtberg [Fri, 4 Dec 2015 19:51:03 +0000 (14:51 -0500)]
Simpler version of gradlemmaU
Anders Mörtberg [Fri, 4 Dec 2015 19:19:41 +0000 (14:19 -0500)]
minor changes
Anders Mörtberg [Fri, 4 Dec 2015 19:01:46 +0000 (14:01 -0500)]
Add the missing line in comp!
Anders Mörtberg [Fri, 4 Dec 2015 16:18:34 +0000 (11:18 -0500)]
another example
Anders Mörtberg [Fri, 4 Dec 2015 16:18:17 +0000 (11:18 -0500)]
remove reglarity
Anders Mörtberg [Fri, 4 Dec 2015 03:52:19 +0000 (22:52 -0500)]
add a shrink function that can be used to not print all of the output
Anders Mörtberg [Fri, 4 Dec 2015 00:57:58 +0000 (19:57 -0500)]
Add VCompU to normal and conv
Anders Mörtberg [Fri, 4 Dec 2015 00:25:12 +0000 (19:25 -0500)]
Add some test of normal forms
Anders Mörtberg [Fri, 4 Dec 2015 00:04:31 +0000 (19:04 -0500)]
Reintroduce compU
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
projects / cubicaltt.git / log