cubicaltt.git
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

9 years agoupdated setTrunc
coquand [Thu, 30 Apr 2015 12:00:22 +0000 (14:00 +0200)]
updated setTrunc

9 years agoadded some test for pi1S2
coquand [Thu, 30 Apr 2015 11:56:57 +0000 (13:56 +0200)]
added some test for pi1S2

9 years agopi1S2 is trivial
coquand [Thu, 30 Apr 2015 11:52:20 +0000 (13:52 +0200)]
pi1S2 is trivial

9 years agopiS2 is trivial
coquand [Thu, 30 Apr 2015 11:44:38 +0000 (13:44 +0200)]
piS2 is trivial

9 years agounivalence
coquand [Thu, 30 Apr 2015 10:23:58 +0000 (12:23 +0200)]
univalence

9 years agothe collection of sets is a groupoid
coquand [Thu, 30 Apr 2015 08:30:52 +0000 (10:30 +0200)]
the collection of sets is a groupoid

9 years agoadded glueLine (wip)
Simon Huber [Wed, 29 Apr 2015 14:16:03 +0000 (16:16 +0200)]
added glueLine (wip)

9 years agoimprove error message
Simon Huber [Wed, 29 Apr 2015 12:19:41 +0000 (14:19 +0200)]
improve error message

9 years agoadded hopf fibration
coquand [Wed, 29 Apr 2015 10:28:10 +0000 (12:28 +0200)]
added hopf fibration

9 years agomore efficient version of groupoid truncation
coquand [Wed, 29 Apr 2015 07:50:57 +0000 (09:50 +0200)]
more efficient version of groupoid truncation

9 years agonicer proof of lemtransport
coquand [Tue, 28 Apr 2015 17:59:04 +0000 (19:59 +0200)]
nicer proof of lemtransport

9 years agoan example of normal form
coquand [Tue, 28 Apr 2015 16:33:36 +0000 (18:33 +0200)]
an example of normal form

9 years agoadded groupoid truncation
coquand [Tue, 28 Apr 2015 11:37:09 +0000 (13:37 +0200)]
added groupoid truncation

9 years agoadded pi1s2
coquand [Tue, 28 Apr 2015 11:22:26 +0000 (13:22 +0200)]
added pi1s2

9 years agoclean mult
coquand [Mon, 27 Apr 2015 19:44:41 +0000 (21:44 +0200)]
clean mult

9 years agoadded some examples for pi1S2
coquand [Mon, 27 Apr 2015 19:42:32 +0000 (21:42 +0200)]
added some examples for pi1S2

9 years agoAdd the test of parsing output from integer back
Anders [Thu, 23 Apr 2015 15:36:31 +0000 (17:36 +0200)]
Add the test of parsing output from integer back

9 years agoFix set
Anders [Thu, 23 Apr 2015 15:26:25 +0000 (17:26 +0200)]
Fix set

9 years agoNormalize formulas
Anders [Thu, 23 Apr 2015 15:26:18 +0000 (17:26 +0200)]
Normalize formulas

9 years agoFix dnf
Anders [Thu, 23 Apr 2015 15:04:11 +0000 (17:04 +0200)]
Fix dnf

9 years agoElimination principle for set truncation
Anders [Thu, 23 Apr 2015 15:04:00 +0000 (17:04 +0200)]
Elimination principle for set truncation

9 years agobugix: take the border of the system where is=js
Simon Huber [Thu, 23 Apr 2015 12:57:28 +0000 (14:57 +0200)]
bugix: take the border of the system where is=js

9 years agoRefactoring of examples
Anders Mörtberg [Tue, 21 Apr 2015 18:19:11 +0000 (20:19 +0200)]
Refactoring of examples

9 years agoAdd normalization of environments
Anders [Tue, 21 Apr 2015 15:59:11 +0000 (17:59 +0200)]
Add normalization of environments

9 years agoproof that mult is an equivalence
coquand [Tue, 21 Apr 2015 15:18:03 +0000 (17:18 +0200)]
proof that mult is an equivalence

9 years agoproof that mult is an equivalence
coquand [Tue, 21 Apr 2015 15:16:20 +0000 (17:16 +0200)]
proof that mult is an equivalence

9 years agoupdated proofs of Hedberg's Theorem
coquand [Tue, 21 Apr 2015 14:57:12 +0000 (16:57 +0200)]
updated proofs of Hedberg's Theorem

9 years agoImprove printing of lambdas and paths
Anders [Tue, 21 Apr 2015 12:38:16 +0000 (14:38 +0200)]
Improve printing of lambdas and paths

9 years agoMake conversion use a list of names instead
Anders [Tue, 21 Apr 2015 10:10:33 +0000 (12:10 +0200)]
Make conversion use a list of names instead

9 years agoRemove unnecessary argument to addBranch
Anders [Tue, 21 Apr 2015 09:44:39 +0000 (11:44 +0200)]
Remove unnecessary argument to addBranch

9 years agoRemove unnecessary monadic code in Typechecker (no more localM!)
Anders [Tue, 21 Apr 2015 09:36:29 +0000 (11:36 +0200)]
Remove unnecessary monadic code in Typechecker (no more localM!)

9 years agoChange ? to !
Anders Mörtberg [Tue, 21 Apr 2015 08:11:02 +0000 (10:11 +0200)]
Change ? to !

9 years agoFix examples
Anders Mörtberg [Tue, 21 Apr 2015 08:10:51 +0000 (10:10 +0200)]
Fix examples

9 years agoUpdate graph script
Anders Mörtberg [Tue, 21 Apr 2015 08:10:39 +0000 (10:10 +0200)]
Update graph script

9 years agoAdd testall
Anders Mörtberg [Tue, 21 Apr 2015 08:10:31 +0000 (10:10 +0200)]
Add testall

9 years agoFix helix
Anders Mörtberg [Tue, 21 Apr 2015 07:48:08 +0000 (09:48 +0200)]
Fix helix

9 years agoFix newhedberg
Anders Mörtberg [Tue, 21 Apr 2015 07:45:24 +0000 (09:45 +0200)]
Fix newhedberg

9 years agoUse old gensym and fresh again
Anders Mörtberg [Tue, 21 Apr 2015 07:45:17 +0000 (09:45 +0200)]
Use old gensym and fresh again

9 years agoFix printing of VPi
Anders Mörtberg [Mon, 20 Apr 2015 21:22:19 +0000 (23:22 +0200)]
Fix printing of VPi

9 years agoFix retract
Anders Mörtberg [Mon, 20 Apr 2015 21:22:12 +0000 (23:22 +0200)]
Fix retract

9 years agoMake normal print nicer names
Anders [Mon, 20 Apr 2015 15:07:21 +0000 (17:07 +0200)]
Make normal print nicer names

9 years agoFix printing of @
Anders [Mon, 20 Apr 2015 14:54:38 +0000 (16:54 +0200)]
Fix printing of @

9 years agoAdd quotient example
Anders [Mon, 20 Apr 2015 14:24:48 +0000 (16:24 +0200)]
Add quotient example

9 years agoSplit higherhit into multiple files
Anders [Mon, 20 Apr 2015 14:10:57 +0000 (16:10 +0200)]
Split higherhit into multiple files

9 years agoMerge remote-tracking branch 'origin/higherhits'
Anders [Mon, 20 Apr 2015 14:03:29 +0000 (16:03 +0200)]
Merge remote-tracking branch 'origin/higherhits'

9 years agoFix the way @ binds (it is now like normal application)
Anders Mörtberg [Mon, 20 Apr 2015 08:34:29 +0000 (10:34 +0200)]
Fix the way @ binds (it is now like normal application)

9 years agoFix a TODO in the resolver (the arguments in a path constructors cannot refer to...
Anders Mörtberg [Mon, 20 Apr 2015 08:26:41 +0000 (10:26 +0200)]
Fix a TODO in the resolver (the arguments in a path constructors cannot refer to the path constructor itself)

9 years agoFix all the old examples of HITs
Anders Mörtberg [Mon, 20 Apr 2015 08:12:57 +0000 (10:12 +0200)]
Fix all the old examples of HITs

9 years agoRemove the @ in PLabel
Anders Mörtberg [Mon, 20 Apr 2015 08:12:37 +0000 (10:12 +0200)]
Remove the @ in PLabel

9 years agoany isomorphism is an equivalence
coquand [Sun, 19 Apr 2015 21:39:47 +0000 (23:39 +0200)]
any isomorphism is an equivalence

9 years agoif A and B are isomorphic, set A -> set B, normal form
coquand [Sun, 19 Apr 2015 13:59:48 +0000 (15:59 +0200)]
if A and B are isomorphic, set A -> set B, normal form

9 years agoif A and B are isomorphic, prop A -> prop B, normal form
coquand [Sun, 19 Apr 2015 13:47:19 +0000 (15:47 +0200)]
if A and B are isomorphic, prop A -> prop B, normal form

9 years agoresult on equivalence of fibers
coquand [Sun, 19 Apr 2015 10:12:08 +0000 (12:12 +0200)]
result on equivalence of fibers

9 years agonew proof of Hedberg's theorem
coquand [Sun, 19 Apr 2015 10:09:20 +0000 (12:09 +0200)]
new proof of Hedberg's theorem

9 years agosome examples
Simon Huber [Sat, 18 Apr 2015 11:50:28 +0000 (13:50 +0200)]
some examples

9 years agolookName error msg for debugging
Simon Huber [Sat, 18 Apr 2015 11:49:45 +0000 (13:49 +0200)]
lookName error msg for debugging

9 years agobugfix in PBranches
Simon Huber [Sat, 18 Apr 2015 11:46:21 +0000 (13:46 +0200)]
bugfix in PBranches

9 years agolet the system in a pcon know about all pcons in the sum
Simon Huber [Sat, 18 Apr 2015 11:44:42 +0000 (13:44 +0200)]
let the system in a pcon know about all pcons in the sum

TODO: the current pcon should not know about itself

9 years agobugfix
Simon Huber [Sat, 18 Apr 2015 03:26:04 +0000 (05:26 +0200)]
bugfix

9 years agobugfix in resolver
Simon Huber [Sat, 18 Apr 2015 02:28:18 +0000 (04:28 +0200)]
bugfix in resolver

9 years agowip (not working yet)
Simon Huber [Sat, 18 Apr 2015 02:08:53 +0000 (04:08 +0200)]
wip (not working yet)

9 years agoFix printing of goals and environments (TODO: Fix "susp (bool)"...)
Anders [Fri, 17 Apr 2015 15:18:04 +0000 (17:18 +0200)]
Fix printing of goals and environments (TODO: Fix "susp (bool)"...)

9 years agoRewrite app and support using case-of
Anders [Fri, 17 Apr 2015 14:20:13 +0000 (16:20 +0200)]
Rewrite app and support using case-of

9 years agoUse Except instead or Error
Anders [Fri, 17 Apr 2015 12:38:07 +0000 (14:38 +0200)]
Use Except instead or Error

9 years agoRemove tabs
Anders [Fri, 17 Apr 2015 12:37:39 +0000 (14:37 +0200)]
Remove tabs

9 years agoOnly show second part of VPi x (VLam ...)
Anders Mörtberg [Fri, 17 Apr 2015 08:50:01 +0000 (10:50 +0200)]
Only show second part of VPi x (VLam ...)

9 years agoAlso normalize the type of lambdas and print VPi nicer
Anders Mörtberg [Fri, 17 Apr 2015 08:35:30 +0000 (10:35 +0200)]
Also normalize the type of lambdas and print VPi nicer

9 years agoUse showTer1 to print closures
Anders Mörtberg [Fri, 17 Apr 2015 07:13:23 +0000 (09:13 +0200)]
Use showTer1 to print closures

9 years agoFix uafunext2
Anders Mörtberg [Fri, 17 Apr 2015 07:13:09 +0000 (09:13 +0200)]
Fix uafunext2

9 years agoRemove some incidentally commited holes
Anders [Thu, 16 Apr 2015 15:18:59 +0000 (17:18 +0200)]
Remove some incidentally commited holes

9 years agoReintroduce _ in identifier again
Anders [Thu, 16 Apr 2015 13:22:53 +0000 (15:22 +0200)]
Reintroduce _ in identifier again

9 years agoreintroduce nicer mkVar
Simon Huber [Thu, 16 Apr 2015 13:15:58 +0000 (15:15 +0200)]
reintroduce nicer mkVar

9 years agokeep name if we have it when generating a fresh name
Simon Huber [Thu, 16 Apr 2015 12:49:14 +0000 (14:49 +0200)]
keep name if we have it when generating a fresh name

9 years agochange mkVar back to how it was
Simon Huber [Thu, 16 Apr 2015 12:32:17 +0000 (14:32 +0200)]
change mkVar back to how it was

9 years agoAdd indentation to Checking and start changing mkVar (not working as expected wrt...
Anders Mörtberg [Thu, 16 Apr 2015 09:18:09 +0000 (11:18 +0200)]
Add indentation to Checking and start changing mkVar (not working as expected wrt holes)

9 years agoOnly print File loaded if file type checks
Anders Mörtberg [Thu, 16 Apr 2015 09:17:30 +0000 (11:17 +0200)]
Only print File loaded if file type checks

9 years agoChange gensym
Anders Mörtberg [Thu, 16 Apr 2015 09:17:12 +0000 (11:17 +0200)]
Change gensym

9 years agoMake holes print the context
Anders Mörtberg [Thu, 16 Apr 2015 09:16:03 +0000 (11:16 +0200)]
Make holes print the context

9 years agoTrailing whitespace
Anders Mörtberg [Thu, 16 Apr 2015 09:13:58 +0000 (11:13 +0200)]
Trailing whitespace

9 years agoFix undefined
Anders Mörtberg [Thu, 16 Apr 2015 09:13:38 +0000 (11:13 +0200)]
Fix undefined

9 years agoFinish example of integers as a HIT
Anders [Wed, 15 Apr 2015 09:47:38 +0000 (11:47 +0200)]
Finish example of integers as a HIT

9 years agoRemove some code from ex1
Anders [Wed, 15 Apr 2015 09:47:20 +0000 (11:47 +0200)]
Remove some code from ex1

9 years agoFix bug in type checker for HITs
Anders [Wed, 15 Apr 2015 09:47:06 +0000 (11:47 +0200)]
Fix bug in type checker for HITs

9 years agoFix undefined
Anders [Wed, 15 Apr 2015 09:46:54 +0000 (11:46 +0200)]
Fix undefined

9 years agoRemove VUndef
Anders Mörtberg [Wed, 15 Apr 2015 08:30:43 +0000 (10:30 +0200)]
Remove VUndef

9 years agoAdd very simple support for holes
Anders Mörtberg [Wed, 15 Apr 2015 08:14:27 +0000 (10:14 +0200)]
Add very simple support for holes

9 years agoMake list compile
Anders Mörtberg [Tue, 14 Apr 2015 21:04:00 +0000 (23:04 +0200)]
Make list compile

9 years agoMake undefined only occur as a declaration so that the type can be inferred
Anders Mörtberg [Tue, 14 Apr 2015 21:03:53 +0000 (23:03 +0200)]
Make undefined only occur as a declaration so that the type can be inferred