projects
/
cubicaltt.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cubicaltt.git
2015-06-05
Simon Huber
Less definitional equalities for glue
commit
|
commitdiff
|
tree
|
snapshot
2015-06-05
Simon Huber
Throw out transport
commit
|
commitdiff
|
tree
|
snapshot
2015-06-05
Simon Huber
Merge branch 'hisoproj' into no_regular
commit
|
commitdiff
|
tree
|
snapshot
2015-06-05
Simon Huber
Finished eqToIso and removed constants for comp in U
commit
|
commitdiff
|
tree
|
snapshot
2015-06-04
Anders Mörtberg
Update squeezeHIT
commit
|
commitdiff
|
tree
|
snapshot
2015-06-04
Simon Huber
Equality to isomorphism (wip)
commit
|
commitdiff
|
tree
|
snapshot
2015-06-04
Anders Mörtberg
define trans in terms of gencomp
commit
|
commitdiff
|
tree
|
snapshot
2015-06-04
Simon Huber
Added fill as a term and comp is now genComp
commit
|
commitdiff
|
tree
|
snapshot
2015-06-04
Anders
Add genComp and some examples for debugging
commit
|
commitdiff
|
tree
|
snapshot
2015-06-04
Anders
remove commented code
commit
|
commitdiff
|
tree
|
snapshot
2015-06-04
Simon Huber
Adapted HITs
commit
|
commitdiff
|
tree
|
snapshot
2015-06-04
Simon Huber
Fix for neutral unglues
commit
|
commitdiff
|
tree
|
snapshot
2015-06-04
Simon Huber
Added neutral values for unglue
commit
|
commitdiff
|
tree
|
snapshot
2015-06-04
Simon Huber
Adapted
commit
|
commitdiff
|
tree
|
snapshot
2015-06-04
Simon Huber
Added constructor for comp in U
commit
|
commitdiff
|
tree
|
snapshot
2015-06-03
Simon Huber
Fix use of compLine
commit
|
commitdiff
|
tree
|
snapshot
2015-06-03
Anders Mörtberg
Fix add_comm
commit
|
commitdiff
|
tree
|
snapshot
2015-06-03
Anders
isNeutralComp, small fixes to comp and comment things...
commit
|
commitdiff
|
tree
|
snapshot
2015-06-03
Simon Huber
Adapted prelude
commit
|
commitdiff
|
tree
|
snapshot
2015-06-03
Simon Huber
Finished first version
commit
|
commitdiff
|
tree
|
snapshot
2015-06-03
Simon Huber
Adapted compGlue
commit
|
commitdiff
|
tree
|
snapshot
2015-06-02
Simon Huber
Started adapting for the non-regular setting (wip)
commit
|
commitdiff
|
tree
|
snapshot
2015-05-18
Anders
Add direct proof that s2 is trivial (for the HIT defini...
commit
|
commitdiff
|
tree
|
snapshot
2015-05-16
coquand
simple examples on nat and list
commit
|
commitdiff
|
tree
|
snapshot
2015-05-12
Anders
Isomorphism of the direct and the susp definition of S2
commit
|
commitdiff
|
tree
|
snapshot
2015-05-11
Anders
Fix the bug in transport and add optimizations to compE...
commit
|
commitdiff
|
tree
|
snapshot
2015-05-08
Anders
Add exchange law and genPiS3
commit
|
commitdiff
|
tree
|
snapshot
2015-05-08
Anders
Change order in checkPathSystem
commit
|
commitdiff
|
tree
|
snapshot
2015-05-06
Anders
Add check that systems don't contain the same face...
commit
|
commitdiff
|
tree
|
snapshot
2015-05-06
Anders
The loop space of the torus is equal to Z * Z
commit
|
commitdiff
|
tree
|
snapshot
2015-05-06
Anders
Cleaning
commit
|
commitdiff
|
tree
|
snapshot
2015-05-06
Anders
Clean helix
commit
|
commitdiff
|
tree
|
snapshot
2015-05-06
Anders
More efficient implementation of environments
commit
|
commitdiff
|
tree
|
snapshot
2015-05-05
Anders Mörtberg
Comment the two slowest tests in mystery
commit
|
commitdiff
|
tree
|
snapshot
2015-05-05
Anders Mörtberg
Add optimization to act
commit
|
commitdiff
|
tree
|
snapshot
2015-05-05
Anders Mörtberg
Add new proof that loopS1 is a set
commit
|
commitdiff
|
tree
|
snapshot
2015-05-05
mortberg
Merge pull request #10 from dlicata335/master
commit
|
commitdiff
|
tree
|
snapshot
2015-05-05
Dan Licata
cleaned up mystery.ctt for inclusion in repository...
commit
|
commitdiff
|
tree
|
snapshot
2015-05-05
Anders Mörtberg
Swap test2 and test3 to correspond to what is in cubical
commit
|
commitdiff
|
tree
|
snapshot
2015-05-05
Anders Mörtberg
Add fix to comp for sums
commit
|
commitdiff
|
tree
|
snapshot
2015-05-04
Anders Mörtberg
Add pi4s3 until test0To5
commit
|
commitdiff
|
tree
|
snapshot
2015-05-04
Anders Mörtberg
Add -t flag
commit
|
commitdiff
|
tree
|
snapshot
2015-05-04
Simon Huber
nicer error msg
commit
|
commitdiff
|
tree
|
snapshot
2015-05-04
Simon Huber
fixed printing of glueLine
commit
|
commitdiff
|
tree
|
snapshot
2015-05-04
Simon Huber
move neutrality test in app of a split to a composition
commit
|
commitdiff
|
tree
|
snapshot
2015-05-04
Simon Huber
use unqualified mapWithKey
commit
|
commitdiff
|
tree
|
snapshot
2015-05-03
Anders Mörtberg
Add missing spaces
commit
|
commitdiff
|
tree
|
snapshot
2015-05-03
mortberg
Merge pull request #9 from dlicata335/master
commit
|
commitdiff
|
tree
|
snapshot
2015-05-02
Dan Licata
six is not the successor of six
commit
|
commitdiff
|
tree
|
snapshot
2015-05-02
Dan Licata
mystery example: beta reduce some compIds
commit
|
commitdiff
|
tree
|
snapshot
2015-05-02
Dan Licata
compile with -rtsopts so you can set the stack space
commit
|
commitdiff
|
tree
|
snapshot
2015-05-02
Dan Licata
use synthetic homotopy theory to get a function on...
commit
|
commitdiff
|
tree
|
snapshot
2015-05-02
Dan Licata
use synthetic homotopy theory to get a function on...
commit
|
commitdiff
|
tree
|
snapshot
2015-05-01
Dan Licata
torus = two circles proof cleanup
commit
|
commitdiff
|
tree
|
snapshot
2015-05-01
Dan Licata
torus = two circles proof
commit
|
commitdiff
|
tree
|
snapshot
2015-04-30
Simon Huber
add more parentheses
commit
|
commitdiff
|
tree
|
snapshot
2015-04-30
Simon Huber
non-trivial homotopy in the loop space of stwo
commit
|
commitdiff
|
tree
|
snapshot
2015-04-30
Simon Huber
allow overshadowing of names
commit
|
commitdiff
|
tree
|
snapshot
2015-04-30
coquand
updated collection
commit
|
commitdiff
|
tree
|
snapshot
2015-04-30
coquand
updated setTrunc
commit
|
commitdiff
|
tree
|
snapshot
2015-04-30
coquand
added some test for pi1S2
commit
|
commitdiff
|
tree
|
snapshot
2015-04-30
coquand
pi1S2 is trivial
commit
|
commitdiff
|
tree
|
snapshot
2015-04-30
coquand
piS2 is trivial
commit
|
commitdiff
|
tree
|
snapshot
2015-04-30
coquand
univalence
commit
|
commitdiff
|
tree
|
snapshot
2015-04-30
coquand
the collection of sets is a groupoid
commit
|
commitdiff
|
tree
|
snapshot
2015-04-29
Simon Huber
added glueLine (wip)
commit
|
commitdiff
|
tree
|
snapshot
2015-04-29
Simon Huber
improve error message
commit
|
commitdiff
|
tree
|
snapshot
2015-04-29
coquand
added hopf fibration
commit
|
commitdiff
|
tree
|
snapshot
2015-04-29
coquand
more efficient version of groupoid truncation
commit
|
commitdiff
|
tree
|
snapshot
2015-04-28
coquand
nicer proof of lemtransport
commit
|
commitdiff
|
tree
|
snapshot
2015-04-28
coquand
an example of normal form
commit
|
commitdiff
|
tree
|
snapshot
2015-04-28
coquand
added groupoid truncation
commit
|
commitdiff
|
tree
|
snapshot
2015-04-28
coquand
added pi1s2
commit
|
commitdiff
|
tree
|
snapshot
2015-04-27
coquand
clean mult
commit
|
commitdiff
|
tree
|
snapshot
2015-04-27
coquand
added some examples for pi1S2
commit
|
commitdiff
|
tree
|
snapshot
2015-04-23
Anders
Add the test of parsing output from integer back
commit
|
commitdiff
|
tree
|
snapshot
2015-04-23
Anders
Fix set
commit
|
commitdiff
|
tree
|
snapshot
2015-04-23
Anders
Normalize formulas
commit
|
commitdiff
|
tree
|
snapshot
2015-04-23
Anders
Fix dnf
commit
|
commitdiff
|
tree
|
snapshot
2015-04-23
Anders
Elimination principle for set truncation
commit
|
commitdiff
|
tree
|
snapshot
2015-04-23
Simon Huber
bugix: take the border of the system where is=js
commit
|
commitdiff
|
tree
|
snapshot
2015-04-21
Anders Mörtberg
Refactoring of examples
commit
|
commitdiff
|
tree
|
snapshot
2015-04-21
Anders
Add normalization of environments
commit
|
commitdiff
|
tree
|
snapshot
2015-04-21
coquand
proof that mult is an equivalence
commit
|
commitdiff
|
tree
|
snapshot
2015-04-21
coquand
proof that mult is an equivalence
commit
|
commitdiff
|
tree
|
snapshot
2015-04-21
coquand
updated proofs of Hedberg's Theorem
commit
|
commitdiff
|
tree
|
snapshot
2015-04-21
Anders
Improve printing of lambdas and paths
commit
|
commitdiff
|
tree
|
snapshot
2015-04-21
Anders
Make conversion use a list of names instead
commit
|
commitdiff
|
tree
|
snapshot
2015-04-21
Anders
Remove unnecessary argument to addBranch
commit
|
commitdiff
|
tree
|
snapshot
2015-04-21
Anders
Remove unnecessary monadic code in Typechecker (no...
commit
|
commitdiff
|
tree
|
snapshot
2015-04-21
Anders Mörtberg
Change ? to !
commit
|
commitdiff
|
tree
|
snapshot
2015-04-21
Anders Mörtberg
Fix examples
commit
|
commitdiff
|
tree
|
snapshot
2015-04-21
Anders Mörtberg
Update graph script
commit
|
commitdiff
|
tree
|
snapshot
2015-04-21
Anders Mörtberg
Add testall
commit
|
commitdiff
|
tree
|
snapshot
2015-04-21
Anders Mörtberg
Fix helix
commit
|
commitdiff
|
tree
|
snapshot
2015-04-21
Anders Mörtberg
Fix newhedberg
commit
|
commitdiff
|
tree
|
snapshot
2015-04-21
Anders Mörtberg
Use old gensym and fresh again
commit
|
commitdiff
|
tree
|
snapshot
2015-04-20
Anders Mörtberg
Fix printing of VPi
commit
|
commitdiff
|
tree
|
snapshot
2015-04-20
Anders Mörtberg
Fix retract
commit
|
commitdiff
|
tree
|
snapshot
2015-04-20
Anders
Make normal print nicer names
commit
|
commitdiff
|
tree
|
snapshot
next