cubicaltt.git
8 years agoAdd warning about recursive HITs
Auke Booij [Thu, 2 Jun 2016 22:47:41 +0000 (23:47 +0100)]
Add warning about recursive HITs

8 years agoRename truncP to inh
Auke Booij [Thu, 2 Jun 2016 22:44:11 +0000 (23:44 +0100)]
Rename truncP to inh

8 years agoimplement propositional truncation
Auke Booij [Wed, 1 Jun 2016 14:41:30 +0000 (15:41 +0100)]
implement propositional truncation

8 years agoadd reserved keywords to README
Anders Mörtberg [Tue, 24 May 2016 15:58:53 +0000 (11:58 -0400)]
add reserved keywords to README

8 years agosmall change
Thierry Coquand [Wed, 27 Apr 2016 09:27:47 +0000 (11:27 +0200)]
small change

8 years agowe should improve the evaluator
Thierry Coquand [Wed, 27 Apr 2016 09:22:34 +0000 (11:22 +0200)]
we should improve the evaluator

8 years agoFinish binnat example and add elimination principles for equivalences and isomorphisms
Anders Mörtberg [Thu, 14 Apr 2016 18:13:02 +0000 (14:13 -0400)]
Finish binnat example and add elimination principles for equivalences and isomorphisms

8 years agoStart porting binnat
Anders Mörtberg [Tue, 12 Apr 2016 21:50:54 +0000 (17:50 -0400)]
Start porting binnat

8 years agoother proof of lemPropF
Thierry Coquand [Fri, 8 Apr 2016 07:09:00 +0000 (09:09 +0200)]
other proof of lemPropF

8 years agosome computations
Thierry Coquand [Sat, 2 Apr 2016 11:49:45 +0000 (13:49 +0200)]
some computations

8 years agostudy of multiplication on S1
Thierry Coquand [Fri, 1 Apr 2016 10:26:27 +0000 (12:26 +0200)]
study of multiplication on S1

8 years agoproof that S1 is a groupoid
Thierry Coquand [Fri, 1 Apr 2016 10:22:28 +0000 (12:22 +0200)]
proof that S1 is a groupoid

8 years agoMerge pull request #36 from georgydunaev/master
Anders Mörtberg [Sun, 6 Mar 2016 14:51:28 +0000 (09:51 -0500)]
Merge pull request #36 from georgydunaev/master

added imports and changed examples/collection.ctt (corrUniv B A)

8 years agoadded imports and changed collection.ctt (corrUniv B A)
Georgy Dunaev [Sun, 6 Mar 2016 09:06:12 +0000 (12:06 +0300)]
added imports and changed collection.ctt (corrUniv B A)

8 years agoFix squeezeHIT for non-recursive HITs
Simon Huber [Thu, 3 Mar 2016 16:31:39 +0000 (17:31 +0100)]
Fix squeezeHIT for non-recursive HITs

8 years agoAnders bugfix for squeezes
Simon Huber [Thu, 3 Mar 2016 12:38:15 +0000 (13:38 +0100)]
Anders bugfix for squeezes

8 years agoMerge pull request #29 from abooij/master
Anders Mörtberg [Thu, 18 Feb 2016 05:54:50 +0000 (00:54 -0500)]
Merge pull request #29 from abooij/master

Soften version constraints

8 years agoSoften version constraints
Auke Booij [Wed, 17 Feb 2016 15:46:18 +0000 (15:46 +0000)]
Soften version constraints

8 years agoFix printing of environments
Simon Huber [Thu, 11 Feb 2016 12:31:33 +0000 (13:31 +0100)]
Fix printing of environments

8 years agoTest for correct length in checks (Fixes #27)
Simon Huber [Wed, 10 Feb 2016 20:31:41 +0000 (21:31 +0100)]
Test for correct length in checks (Fixes #27)

8 years agoadd a small test of the grad lemma
Anders Mörtberg [Wed, 27 Jan 2016 20:35:27 +0000 (15:35 -0500)]
add a small test of the grad lemma

8 years agocleaning
Anders Mörtberg [Sat, 23 Jan 2016 17:51:36 +0000 (12:51 -0500)]
cleaning

8 years agoMerge branch 'nunivalence'
Anders Mörtberg [Sat, 23 Jan 2016 17:40:21 +0000 (12:40 -0500)]
Merge branch 'nunivalence'

8 years agocomment in nthmUniv
Anders Mörtberg [Sat, 23 Jan 2016 17:38:16 +0000 (12:38 -0500)]
comment in nthmUniv

8 years agoadd the correct normal form of univalence
Anders Mörtberg [Sat, 23 Jan 2016 17:36:05 +0000 (12:36 -0500)]
add the correct normal form of univalence

8 years agouse uahp' in setquot instead
Anders Mörtberg [Sat, 23 Jan 2016 17:32:56 +0000 (12:32 -0500)]
use uahp' in setquot instead

8 years agoFix ö
Anders Mörtberg [Wed, 20 Jan 2016 14:00:09 +0000 (09:00 -0500)]
Fix ö

8 years agoUpdated readme
Simon Huber [Wed, 20 Jan 2016 10:44:39 +0000 (11:44 +0100)]
Updated readme

8 years agoMissing case for checking GlueElem against VCompU
Simon Huber [Mon, 18 Jan 2016 10:42:15 +0000 (11:42 +0100)]
Missing case for checking GlueElem against VCompU

8 years agomove two lemmas to nat
Anders Mörtberg [Fri, 15 Jan 2016 21:29:06 +0000 (16:29 -0500)]
move two lemmas to nat

8 years agofinish the hz exercise
Anders Mörtberg [Fri, 15 Jan 2016 21:05:40 +0000 (16:05 -0500)]
finish the hz exercise

8 years agoFinish the last undefined in setquot
Anders Mörtberg [Fri, 15 Jan 2016 19:08:23 +0000 (14:08 -0500)]
Finish the last undefined in setquot

8 years ago"fix" bug
Anders Mörtberg [Fri, 15 Jan 2016 16:49:15 +0000 (11:49 -0500)]
"fix" bug

8 years agoBugfix in inferType
Simon Huber [Fri, 15 Jan 2016 16:38:32 +0000 (17:38 +0100)]
Bugfix in inferType

8 years agosetquot is a set
Anders Mörtberg [Fri, 15 Jan 2016 03:55:34 +0000 (22:55 -0500)]
setquot is a set

8 years agoone less undefined
Anders Mörtberg [Fri, 15 Jan 2016 03:44:12 +0000 (22:44 -0500)]
one less undefined

8 years agosquash some admits
Anders Mörtberg [Fri, 15 Jan 2016 03:22:41 +0000 (22:22 -0500)]
squash some admits

8 years agominor changes
Anders Mörtberg [Thu, 14 Jan 2016 23:21:50 +0000 (18:21 -0500)]
minor changes

8 years agomore on setquot. on the way to define an equality test for hz
Anders Mörtberg [Thu, 14 Jan 2016 21:56:45 +0000 (16:56 -0500)]
more on setquot. on the way to define an equality test for hz

8 years agoadd nlem1
Anders Mörtberg [Thu, 14 Jan 2016 15:36:33 +0000 (10:36 -0500)]
add nlem1

8 years agoChange printing of environments
Anders Mörtberg [Thu, 14 Jan 2016 15:33:34 +0000 (10:33 -0500)]
Change printing of environments

8 years agorename sig to Sigma and make setquot compile
Anders Mörtberg [Thu, 14 Jan 2016 15:33:23 +0000 (10:33 -0500)]
rename sig to Sigma and make setquot compile

8 years agomake bool compile and move tests using univalence for bool
Anders Mörtberg [Thu, 14 Jan 2016 14:59:51 +0000 (09:59 -0500)]
make bool compile and move tests using univalence for bool

8 years agoBugfix in compU and compGlue
Simon Huber [Thu, 14 Jan 2016 14:19:03 +0000 (15:19 +0100)]
Bugfix in compU and compGlue

8 years agoBugfix by Fabian Ruch
Simon Huber [Tue, 12 Jan 2016 11:08:23 +0000 (12:08 +0100)]
Bugfix by Fabian Ruch

8 years agofix bug
Anders Mörtberg [Sat, 9 Jan 2016 11:50:12 +0000 (12:50 +0100)]
fix bug

8 years agocleaning
Anders Mörtberg [Fri, 8 Jan 2016 09:54:54 +0000 (10:54 +0100)]
cleaning

8 years agocomment gradLemmaU
Anders Mörtberg [Thu, 7 Jan 2016 17:05:29 +0000 (18:05 +0100)]
comment gradLemmaU

8 years agoremove @@@
Anders Mörtberg [Thu, 7 Jan 2016 17:05:22 +0000 (18:05 +0100)]
remove @@@

8 years agodont write to a file
Anders Mörtberg [Thu, 7 Jan 2016 17:03:01 +0000 (18:03 +0100)]
dont write to a file

8 years ago"_" in constPath again
Anders Mörtberg [Thu, 7 Jan 2016 17:02:27 +0000 (18:02 +0100)]
"_" in constPath again

8 years agouse compConstLine
Anders Mörtberg [Tue, 5 Jan 2016 11:50:54 +0000 (12:50 +0100)]
use compConstLine

8 years agoadd the huge normal form of corrUniv which trigger the bug
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

8 years agoremove a space in a comment
Anders Mörtberg [Tue, 5 Jan 2016 11:19:45 +0000 (12:19 +0100)]
remove a space in a comment

8 years agochange constPath to avoid strange bug
Anders Mörtberg [Tue, 5 Jan 2016 11:07:56 +0000 (12:07 +0100)]
change constPath to avoid strange bug

8 years agocomment
Anders Mörtberg [Tue, 5 Jan 2016 11:07:45 +0000 (12:07 +0100)]
comment

8 years agoadd parsing of ! in beginning of idents
Anders Mörtberg [Tue, 5 Jan 2016 11:07:39 +0000 (12:07 +0100)]
add parsing of ! in beginning of idents

8 years agoremove all <_>
Anders Mörtberg [Tue, 5 Jan 2016 09:21:54 +0000 (10:21 +0100)]
remove all <_>

8 years agochange printing of compU
Anders Mörtberg [Tue, 5 Jan 2016 09:21:22 +0000 (10:21 +0100)]
change printing of compU

8 years agoadded an example with ordinals
coquand [Mon, 4 Jan 2016 16:58:17 +0000 (17:58 +0100)]
added an example with ordinals

8 years agoMore cleaning
Anders Mörtberg [Mon, 4 Jan 2016 19:03:31 +0000 (20:03 +0100)]
More cleaning

8 years agoAdd bool example to univalence.ctt
Anders Mörtberg [Mon, 4 Jan 2016 18:47:44 +0000 (19:47 +0100)]
Add bool example to univalence.ctt

8 years agoCleaning and removal of duplicate code. Put all proofs of univalence in the same...
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

8 years agoRefactoring and move old code on equivalences to experiments folder
Anders Mörtberg [Mon, 4 Jan 2016 18:18:40 +0000 (19:18 +0100)]
Refactoring and move old code on equivalences to experiments folder

8 years agoMake aim.ctt compile
Anders Mörtberg [Thu, 31 Dec 2015 08:03:46 +0000 (09:03 +0100)]
Make aim.ctt compile

8 years agoMerge branch 'compU'
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

8 years agoMerge branch 'testUniv'
Anders Mörtberg [Thu, 31 Dec 2015 07:24:29 +0000 (08:24 +0100)]
Merge branch 'testUniv'

# Conflicts:
# examples/testContr.ctt
# examples/testEquiv.ctt

8 years agoupdate aim.ctt
Anders Mörtberg [Thu, 31 Dec 2015 07:15:53 +0000 (08:15 +0100)]
update aim.ctt

8 years agoadd standard formulation of univalence
Anders Mörtberg [Wed, 30 Dec 2015 18:58:37 +0000 (19:58 +0100)]
add standard formulation of univalence

8 years agoan example of normal form
coquand [Wed, 30 Dec 2015 10:13:46 +0000 (11:13 +0100)]
an example of normal form

8 years agoupdated collection
coquand [Tue, 29 Dec 2015 15:16:37 +0000 (16:16 +0100)]
updated collection

8 years agosmall change
coquand [Tue, 29 Dec 2015 15:04:44 +0000 (16:04 +0100)]
small change

8 years agoupdated sigma, not use of J
coquand [Tue, 29 Dec 2015 15:03:42 +0000 (16:03 +0100)]
updated sigma, not use of J

8 years agoupdated multS1
coquand [Tue, 29 Dec 2015 14:52:35 +0000 (15:52 +0100)]
updated multS1

8 years agocircle now works with this version of univalence
coquand [Tue, 29 Dec 2015 11:42:12 +0000 (12:42 +0100)]
circle now works with this version of univalence

8 years agochanged compU
coquand [Sun, 27 Dec 2015 18:33:04 +0000 (19:33 +0100)]
changed compU

8 years agosimple tests for univalence
coquand [Sun, 27 Dec 2015 09:09:05 +0000 (10:09 +0100)]
simple tests for univalence

8 years agoneutral for compU
coquand [Sun, 27 Dec 2015 08:59:19 +0000 (09:59 +0100)]
neutral for compU

8 years agoMakefile
coquand [Sat, 26 Dec 2015 19:49:27 +0000 (20:49 +0100)]
Makefile

8 years agoother proof of univalence
coquand [Sat, 26 Dec 2015 19:45:35 +0000 (20:45 +0100)]
other proof of univalence

8 years agocorrected Eval
coquand [Sat, 26 Dec 2015 19:22:53 +0000 (20:22 +0100)]
corrected Eval

8 years agoan example where we type-checked a normal form
coquand [Sat, 26 Dec 2015 19:02:12 +0000 (20:02 +0100)]
an example where we type-checked a normal form

8 years agoproof of univalence?
coquand [Sat, 26 Dec 2015 17:27:18 +0000 (18:27 +0100)]
proof of univalence?

8 years agounivalence
coquand [Sat, 26 Dec 2015 16:35:18 +0000 (17:35 +0100)]
univalence

8 years agoproof of univalence
coquand [Sat, 26 Dec 2015 16:14:38 +0000 (17:14 +0100)]
proof of univalence

8 years agoupdated testContr
coquand [Sat, 26 Dec 2015 12:26:42 +0000 (13:26 +0100)]
updated testContr

8 years agosome lemmas about contractible types
coquand [Tue, 22 Dec 2015 13:52:11 +0000 (14:52 +0100)]
some lemmas about contractible types

8 years agotestEquiv
coquand [Sat, 19 Dec 2015 18:25:41 +0000 (19:25 +0100)]
testEquiv

8 years agosimplified transIdFun
coquand [Sat, 19 Dec 2015 18:04:59 +0000 (19:04 +0100)]
simplified transIdFun

8 years agosimpler version of idToId in testEquiv
coquand [Fri, 18 Dec 2015 20:42:17 +0000 (21:42 +0100)]
simpler version of idToId in testEquiv

8 years agotestEquiv
coquand [Sat, 19 Dec 2015 18:25:41 +0000 (19:25 +0100)]
testEquiv

8 years agosimplified transIdFun
coquand [Sat, 19 Dec 2015 18:04:59 +0000 (19:04 +0100)]
simplified transIdFun

8 years agosimpler version of idToId in testEquiv
coquand [Fri, 18 Dec 2015 20:42:17 +0000 (21:42 +0100)]
simpler version of idToId in testEquiv

8 years agoalternative definition of equivalences
Anders Mörtberg [Fri, 18 Dec 2015 14:08:27 +0000 (09:08 -0500)]
alternative definition of equivalences

8 years agoFixed eqToEquiv
Simon Huber [Thu, 17 Dec 2015 08:51:52 +0000 (09:51 +0100)]
Fixed eqToEquiv

8 years agoSwitched back to equiv, simplified glue
Simon Huber [Wed, 16 Dec 2015 11:30:48 +0000 (12:30 +0100)]
Switched back to equiv, simplified glue

8 years agoBugfix for type checking glueElems by Fabian Ruch
Simon Huber [Tue, 15 Dec 2015 13:53:36 +0000 (14:53 +0100)]
Bugfix for type checking glueElems by Fabian Ruch

8 years agoEfficient @@ for fresh names
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.

8 years agoSimplified pathComp
Simon Huber [Mon, 14 Dec 2015 14:37:23 +0000 (15:37 +0100)]
Simplified pathComp

8 years agostart working on hz
Anders Mörtberg [Fri, 11 Dec 2015 21:39:35 +0000 (16:39 -0500)]
start working on hz