cubicaltt.git
2016-07-05 Anders Mörtbergwip
2016-07-05 Anders Mörtbergwip on an equivalent presentation of the circle as...
2016-07-05 Anders Mörtbergminor changes to circle
2016-07-01 Simon HuberMerge pull request #39 from abooij/prop-trunc
2016-06-02 Auke BooijAdd warning about recursive HITs
2016-06-02 Auke BooijRename truncP to inh
2016-06-01 Auke Booijimplement propositional truncation
2016-05-24 Anders Mörtbergadd reserved keywords to README
2016-04-27 Thierry Coquandsmall change
2016-04-27 Thierry Coquandwe should improve the evaluator
2016-04-14 Anders MörtbergFinish binnat example and add elimination principles...
2016-04-12 Anders MörtbergStart porting binnat
2016-04-08 Thierry Coquandother proof of lemPropF
2016-04-02 Thierry Coquandsome computations
2016-04-01 Thierry Coquandstudy of multiplication on S1
2016-04-01 Thierry Coquandproof that S1 is a groupoid
2016-03-06 Anders MörtbergMerge pull request #36 from georgydunaev/master
2016-03-06 Georgy Dunaevadded imports and changed collection.ctt (corrUniv...
2016-03-03 Simon HuberFix squeezeHIT for non-recursive HITs
2016-03-03 Simon HuberAnders bugfix for squeezes
2016-02-18 Anders MörtbergMerge pull request #29 from abooij/master
2016-02-17 Auke BooijSoften version constraints
2016-02-11 Simon HuberFix printing of environments
2016-02-10 Simon HuberTest for correct length in checks (Fixes #27)
2016-01-27 Anders Mörtbergadd a small test of the grad lemma
2016-01-23 Anders Mörtbergcleaning
2016-01-23 Anders MörtbergMerge branch 'nunivalence'
2016-01-23 Anders Mörtbergcomment in nthmUniv
2016-01-23 Anders Mörtbergadd the correct normal form of univalence
2016-01-23 Anders Mörtberguse uahp' in setquot instead
2016-01-20 Anders MörtbergFix ö
2016-01-20 Simon HuberUpdated readme
2016-01-18 Simon HuberMissing case for checking GlueElem against VCompU
2016-01-15 Anders Mörtbergmove two lemmas to nat
2016-01-15 Anders Mörtbergfinish the hz exercise
2016-01-15 Anders MörtbergFinish the last undefined in setquot
2016-01-15 Anders Mörtberg"fix" bug
2016-01-15 Simon HuberBugfix in inferType
2016-01-15 Anders Mörtbergsetquot is a set
2016-01-15 Anders Mörtbergone less undefined
2016-01-15 Anders Mörtbergsquash some admits
2016-01-14 Anders Mörtbergminor changes
2016-01-14 Anders Mörtbergmore on setquot. on the way to define an equality test...
2016-01-14 Anders Mörtbergadd nlem1
2016-01-14 Anders MörtbergChange printing of environments
2016-01-14 Anders Mörtbergrename sig to Sigma and make setquot compile
2016-01-14 Anders Mörtbergmake bool compile and move tests using univalence for...
2016-01-14 Simon HuberBugfix in compU and compGlue
2016-01-12 Simon HuberBugfix by Fabian Ruch
2016-01-09 Anders Mörtbergfix bug
2016-01-08 Anders Mörtbergcleaning
2016-01-07 Anders Mörtbergcomment gradLemmaU
2016-01-07 Anders Mörtbergremove @@@
2016-01-07 Anders Mörtbergdont write to a file
2016-01-07 Anders Mörtberg"_" in constPath again
2016-01-05 Anders Mörtberguse compConstLine
2016-01-05 Anders Mörtbergadd the huge normal form of corrUniv which trigger...
2016-01-05 Anders Mörtbergremove a space in a comment
2016-01-05 Anders Mörtbergchange constPath to avoid strange bug
2016-01-05 Anders Mörtbergcomment
2016-01-05 Anders Mörtbergadd parsing of ! in beginning of idents
2016-01-05 Anders Mörtbergremove all <_>
2016-01-05 Anders Mörtbergchange printing of compU
2016-01-04 coquandadded an example with ordinals
2016-01-04 Anders MörtbergMore cleaning
2016-01-04 Anders MörtbergAdd bool example to univalence.ctt
2016-01-04 Anders MörtbergCleaning and removal of duplicate code. Put all proofs...
2016-01-04 Anders MörtbergRefactoring and move old code on equivalences to experi...
2015-12-31 Anders MörtbergMake aim.ctt compile
2015-12-31 Anders MörtbergMerge branch 'compU'
2015-12-31 Anders MörtbergMerge branch 'testUniv'
2015-12-31 Anders Mörtbergupdate aim.ctt
2015-12-30 Anders Mörtbergadd standard formulation of univalence
2015-12-30 coquandan example of normal form
2015-12-29 coquandupdated collection
2015-12-29 coquandsmall change
2015-12-29 coquandupdated sigma, not use of J
2015-12-29 coquandupdated multS1
2015-12-29 coquandcircle now works with this version of univalence
2015-12-27 coquandchanged compU
2015-12-27 coquandsimple tests for univalence
2015-12-27 coquandneutral for compU
2015-12-26 coquandMakefile
2015-12-26 coquandother proof of univalence
2015-12-26 coquandcorrected Eval
2015-12-26 coquandan example where we type-checked a normal form
2015-12-26 coquandproof of univalence?
2015-12-26 coquandunivalence
2015-12-26 coquandproof of univalence
2015-12-26 coquandupdated testContr
2015-12-22 coquandsome lemmas about contractible types
2015-12-19 coquandtestEquiv
2015-12-19 coquandsimplified transIdFun
2015-12-19 coquandsimpler version of idToId in testEquiv
2015-12-19 coquandtestEquiv
2015-12-19 coquandsimplified transIdFun
2015-12-18 coquandsimpler version of idToId in testEquiv
2015-12-18 Anders Mörtbergalternative definition of equivalences
2015-12-17 Simon HuberFixed eqToEquiv
2015-12-16 Simon HuberSwitched back to equiv, simplified glue
next