cubicaltt.git
2015-06-18 AndersReintroduce transport
2015-06-18 AndersReintroduce glueElem
2015-06-17 AndersFinish the proof of univalence
2015-06-17 Anders MörtbergStart adding gradlemma to finish proof of univalence
2015-06-16 Simon HuberA proof of univalence (wip)
2015-06-16 Simon HuberAdds projections for equivs
2015-06-16 Simon HuberTypo
2015-06-16 Simon HuberDon't require equivalences to be eta-expanded
2015-06-15 Simon HuberFinished eqToEquiv
2015-06-09 Simon HuberRename hiso to equiv
2015-06-09 Simon HuberEquivalences instead of isos (wip)
2015-06-08 AndersMake bool, circle and integer compile
2015-06-08 AndersAdd lemSimpl
2015-06-08 Simon HuberConvertability for hComp
2015-06-06 Anders MörtbergUpdate aim.ctt again
2015-06-06 Anders MörtbergUpdate aim.ctt
2015-06-06 Anders MörtbergAdd AIM talk
2015-06-05 Simon HuberLess definitional equalities for glue
2015-06-05 Simon HuberThrow out transport
2015-06-05 Simon HuberMerge branch 'hisoproj' into no_regular
2015-06-05 Simon HuberFinished eqToIso and removed constants for comp in U
2015-06-04 Anders MörtbergUpdate squeezeHIT
2015-06-04 Simon HuberEquality to isomorphism (wip)
2015-06-04 Anders Mörtbergdefine trans in terms of gencomp
2015-06-04 Simon HuberAdded fill as a term and comp is now genComp
2015-06-04 AndersAdd genComp and some examples for debugging
2015-06-04 Andersremove commented code
2015-06-04 Simon HuberAdapted HITs
2015-06-04 Simon HuberFix for neutral unglues
2015-06-04 Simon HuberAdded neutral values for unglue
2015-06-04 Simon HuberAdapted
2015-06-04 Simon HuberAdded constructor for comp in U
2015-06-03 Simon HuberFix use of compLine
2015-06-03 Anders MörtbergFix add_comm
2015-06-03 AndersisNeutralComp, small fixes to comp and comment things...
2015-06-03 Simon HuberAdapted prelude
2015-06-03 Simon HuberFinished first version
2015-06-03 Simon HuberAdapted compGlue
2015-06-02 Simon HuberStarted adapting for the non-regular setting (wip)
2015-05-18 AndersAdd direct proof that s2 is trivial (for the HIT defini...
2015-05-16 coquandsimple examples on nat and list
2015-05-12 AndersIsomorphism of the direct and the susp definition of S2
2015-05-11 AndersFix the bug in transport and add optimizations to compE...
2015-05-08 AndersAdd exchange law and genPiS3
2015-05-08 AndersChange order in checkPathSystem
2015-05-06 AndersAdd check that systems don't contain the same face...
2015-05-06 AndersThe loop space of the torus is equal to Z * Z
2015-05-06 AndersCleaning
2015-05-06 AndersClean helix
2015-05-06 AndersMore efficient implementation of environments
2015-05-05 Anders MörtbergComment the two slowest tests in mystery
2015-05-05 Anders MörtbergAdd optimization to act
2015-05-05 Anders MörtbergAdd new proof that loopS1 is a set
2015-05-05 mortbergMerge pull request #10 from dlicata335/master
2015-05-05 Dan Licatacleaned up mystery.ctt for inclusion in repository...
2015-05-05 Anders MörtbergSwap test2 and test3 to correspond to what is in cubical
2015-05-05 Anders MörtbergAdd fix to comp for sums
2015-05-04 Anders MörtbergAdd pi4s3 until test0To5
2015-05-04 Anders MörtbergAdd -t flag
2015-05-04 Simon Hubernicer error msg
2015-05-04 Simon Huberfixed printing of glueLine
2015-05-04 Simon Hubermove neutrality test in app of a split to a composition
2015-05-04 Simon Huberuse unqualified mapWithKey
2015-05-03 Anders MörtbergAdd missing spaces
2015-05-03 mortbergMerge pull request #9 from dlicata335/master
2015-05-02 Dan Licatasix is not the successor of six
2015-05-02 Dan Licatamystery example: beta reduce some compIds
2015-05-02 Dan Licatacompile with -rtsopts so you can set the stack space
2015-05-02 Dan Licatause synthetic homotopy theory to get a function on...
2015-05-02 Dan Licatause synthetic homotopy theory to get a function on...
2015-05-01 Dan Licatatorus = two circles proof cleanup
2015-05-01 Dan Licatatorus = two circles proof
2015-04-30 Simon Huberadd more parentheses
2015-04-30 Simon Hubernon-trivial homotopy in the loop space of stwo
2015-04-30 Simon Huberallow overshadowing of names
2015-04-30 coquandupdated collection
2015-04-30 coquandupdated setTrunc
2015-04-30 coquandadded some test for pi1S2
2015-04-30 coquandpi1S2 is trivial
2015-04-30 coquandpiS2 is trivial
2015-04-30 coquandunivalence
2015-04-30 coquandthe collection of sets is a groupoid
2015-04-29 Simon Huberadded glueLine (wip)
2015-04-29 Simon Huberimprove error message
2015-04-29 coquandadded hopf fibration
2015-04-29 coquandmore efficient version of groupoid truncation
2015-04-28 coquandnicer proof of lemtransport
2015-04-28 coquandan example of normal form
2015-04-28 coquandadded groupoid truncation
2015-04-28 coquandadded pi1s2
2015-04-27 coquandclean mult
2015-04-27 coquandadded some examples for pi1S2
2015-04-23 AndersAdd the test of parsing output from integer back
2015-04-23 AndersFix set
2015-04-23 AndersNormalize formulas
2015-04-23 AndersFix dnf
2015-04-23 AndersElimination principle for set truncation
2015-04-23 Simon Huberbugix: take the border of the system where is=js
2015-04-21 Anders MörtbergRefactoring of examples
2015-04-21 AndersAdd normalization of environments
next