cubicaltt.git
2015-07-03 coquandremoved some examples (to be updated)
2015-07-03 coquandadded some examples
2015-07-03 coquandMerge branch 'master' of https://github.com/mortberg...
2015-07-03 coquandminor changes
2015-07-03 Anders MörtbergUpdate README
2015-07-02 Anders MörtbergAdd the proof of univalence using glue with isos
2015-07-01 Anders MörtbergFix imports
2015-06-30 Anders MörtbergFix typo in typechecker and redefine isoId using glue
2015-06-30 Anders MörtbergRevert to using iso instead of equiv
2015-06-29 AndersSome lemmas about equivs
2015-06-29 AndersUpdate aim talk
2015-06-28 Simon HuberFixed lemCompInv
2015-06-24 Simon HuberEquations for subst and J
2015-06-22 Simon HuberFix typo in inferType
2015-06-18 AndersRestate univalence
2015-06-18 AndersUpdate susp
2015-06-18 AndersUpdate README and update demo.ctt
2015-06-18 AndersCleaning and reorganization of files
2015-06-18 AndersMerge branch 'no_regular' into equiv
2015-06-18 AndersCleaning
2015-06-18 AndersAdd typechecking for glueElem
2015-06-18 AndersRemove old code for eqToIso and gradLemma for isos
2015-06-18 AndersMake more names unqualified when importing Map and...
2015-06-18 AndersImprove printing of fst and snd
2015-06-18 AndersRemove commented code for GlueLine, GlueLineElem, CompE...
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-15 Simon HuberFix handling of neutral for composition in sums
2015-06-13 AndersFix hisos''
2015-06-12 AndersFix printing
2015-06-10 Simon HuberConvertability for HSum
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
next