projects / cubicaltt.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cubicaltt.git
2016-07-07 Anders Mörtbergmove ex1 into circle commit | commitdiff | tree | snapshot
2016-07-07 Anders Mörtbergremove duplicate code commit | commitdiff | tree | snapshot
2016-07-07 Anders Mörtbergadd a line without any specified points commit | commitdiff | tree | snapshot
2016-07-07 Anders MörtbergMerge branch 'csystems' commit | commitdiff | tree | snapshot
2016-07-06 Anders Mörtbergdon't hardcode list of ctt files in Makefile for genera... commit | commitdiff | tree | snapshot
2016-07-06 Anders Mörtbergcleaning in prelude commit | commitdiff | tree | snapshot
2016-07-06 Anders Mörtbergadd equalNat commit | commitdiff | tree | snapshot
2016-07-05 Anders Mörtbergfix name of local splits commit | commitdiff | tree | snapshot
2016-07-05 Anders Mörtbergadd local split commit | commitdiff | tree | snapshot
2016-07-05 Anders Mörtbergadd batch mode flag commit | commitdiff | tree | snapshot
2016-07-05 Anders Mörtbergwip commit | commitdiff | tree | snapshot
2016-07-05 Anders Mörtbergwip on an equivalent presentation of the circle as... commit | commitdiff | tree | snapshot
2016-07-05 Anders Mörtbergminor changes to circle commit | commitdiff | tree | snapshot
2016-07-01 Simon HuberMerge pull request #39 from abooij/prop-trunc commit | commitdiff | tree | snapshot
2016-06-20 Rafaël BocquetTwo equivalent categories are equal commit | commitdiff | tree | snapshot
2016-06-14 Rafaël Bocquetwip commit | commitdiff | tree | snapshot
2016-06-13 Rafaël Bocquetwip commit | commitdiff | tree | snapshot
2016-06-02 Auke BooijAdd warning about recursive HITs commit | commitdiff | tree | snapshot
2016-06-02 Auke BooijRename truncP to inh commit | commitdiff | tree | snapshot
2016-06-01 Auke Booijimplement propositional truncation commit | commitdiff | tree | snapshot
2016-05-31 Rafaël BocquetSplit csystem.ctt into category.ctt and csystem.ctt commit | commitdiff | tree | snapshot
2016-05-24 Anders Mörtbergadd reserved keywords to README commit | commitdiff | tree | snapshot
2016-05-23 Rafaël BocquetConstruction of a C0-System from a universe category commit | commitdiff | tree | snapshot
2016-05-23 Rafaël BocquetFix the module name commit | commitdiff | tree | snapshot
2016-05-23 Rafaël Bocquet(wip) construction of a C0-System from a universe category commit | commitdiff | tree | snapshot
2016-05-10 Rafaël BocquetBoth definitions of C systems; the second one implies... commit | commitdiff | tree | snapshot
2016-04-27 Thierry Coquandsmall change commit | commitdiff | tree | snapshot
2016-04-27 Thierry Coquandwe should improve the evaluator commit | commitdiff | tree | snapshot
2016-04-21 Rafaël BocquetMerge branch 'master' of github.com:mortberg/cubicaltt... commit | commitdiff | tree | snapshot
2016-04-21 Rafaël Bocquetdefinition of C systems commit | commitdiff | tree | snapshot
2016-04-14 Anders MörtbergFinish binnat example and add elimination principles... commit | commitdiff | tree | snapshot
2016-04-14 Rafaël Bocquetsimple computation using multZ commit | commitdiff | tree | snapshot
2016-04-14 Rafaël Bocquettorsor multiplication commit | commitdiff | tree | snapshot
2016-04-13 Rafaël Bocqueteval ignores opaqueness commit | commitdiff | tree | snapshot
2016-04-12 Anders MörtbergStart porting binnat commit | commitdiff | tree | snapshot
2016-04-12 Rafaël Bocquetvisible_all command commit | commitdiff | tree | snapshot
2016-04-12 Rafaël BocquetOpaque/Visible definitions commit | commitdiff | tree | snapshot
2016-04-08 Rafaël Bocquetsome proofs commit | commitdiff | tree | snapshot
2016-04-08 Rafaël Bocquetslow proof commit | commitdiff | tree | snapshot
2016-04-08 Thierry Coquandother proof of lemPropF commit | commitdiff | tree | snapshot
2016-04-07 Rafaël BocquetOnly ZEquiv : isEquiv (plus x) is not proven commit | commitdiff | tree | snapshot
2016-04-06 Rafaël BocquetS1 = BZ commit | commitdiff | tree | snapshot
2016-04-05 Rafaël BocquetMerge branch 'master' of https://github.com/mortberg... commit | commitdiff | tree | snapshot
2016-04-05 Rafaël BocquetZ = Id BZ ZBZ ZBZ commit | commitdiff | tree | snapshot
2016-04-04 Rafaël Bocquet. commit | commitdiff | tree | snapshot
2016-04-02 Thierry Coquandsome computations commit | commitdiff | tree | snapshot
2016-04-01 Thierry Coquandstudy of multiplication on S1 commit | commitdiff | tree | snapshot
2016-04-01 Thierry Coquandproof that S1 is a groupoid commit | commitdiff | tree | snapshot
2016-03-06 Anders MörtbergMerge pull request #36 from georgydunaev/master commit | commitdiff | tree | snapshot
2016-03-06 Georgy Dunaevadded imports and changed collection.ctt (corrUniv... commit | commitdiff | tree | snapshot
2016-03-03 Simon HuberFix squeezeHIT for non-recursive HITs commit | commitdiff | tree | snapshot
2016-03-03 Simon HuberAnders bugfix for squeezes commit | commitdiff | tree | snapshot
2016-02-18 Anders MörtbergMerge pull request #29 from abooij/master commit | commitdiff | tree | snapshot
2016-02-17 Auke BooijSoften version constraints commit | commitdiff | tree | snapshot
2016-02-11 Simon HuberFix printing of environments commit | commitdiff | tree | snapshot
2016-02-10 Simon HuberTest for correct length in checks (Fixes #27) commit | commitdiff | tree | snapshot
2016-01-27 Anders Mörtbergadd a small test of the grad lemma commit | commitdiff | tree | snapshot
2016-01-23 Anders Mörtbergcleaning commit | commitdiff | tree | snapshot
2016-01-23 Anders MörtbergMerge branch 'nunivalence' commit | commitdiff | tree | snapshot
2016-01-23 Anders Mörtbergcomment in nthmUniv commit | commitdiff | tree | snapshot
2016-01-23 Anders Mörtbergadd the correct normal form of univalence commit | commitdiff | tree | snapshot
2016-01-23 Anders Mörtberguse uahp' in setquot instead commit | commitdiff | tree | snapshot
2016-01-20 Anders MörtbergFix ö commit | commitdiff | tree | snapshot
2016-01-20 Simon HuberUpdated readme commit | commitdiff | tree | snapshot
2016-01-18 Simon HuberMissing case for checking GlueElem against VCompU commit | commitdiff | tree | snapshot
2016-01-15 Anders Mörtbergmove two lemmas to nat commit | commitdiff | tree | snapshot
2016-01-15 Anders Mörtbergfinish the hz exercise commit | commitdiff | tree | snapshot
2016-01-15 Anders MörtbergFinish the last undefined in setquot commit | commitdiff | tree | snapshot
2016-01-15 Anders Mörtberg"fix" bug commit | commitdiff | tree | snapshot
2016-01-15 Simon HuberBugfix in inferType commit | commitdiff | tree | snapshot
2016-01-15 Anders Mörtbergsetquot is a set commit | commitdiff | tree | snapshot
2016-01-15 Anders Mörtbergone less undefined commit | commitdiff | tree | snapshot
2016-01-15 Anders Mörtbergsquash some admits commit | commitdiff | tree | snapshot
2016-01-14 Anders Mörtbergminor changes commit | commitdiff | tree | snapshot
2016-01-14 Anders Mörtbergmore on setquot. on the way to define an equality test... commit | commitdiff | tree | snapshot
2016-01-14 Anders Mörtbergadd nlem1 commit | commitdiff | tree | snapshot
2016-01-14 Anders MörtbergChange printing of environments commit | commitdiff | tree | snapshot
2016-01-14 Anders Mörtbergrename sig to Sigma and make setquot compile commit | commitdiff | tree | snapshot
2016-01-14 Anders Mörtbergmake bool compile and move tests using univalence for... commit | commitdiff | tree | snapshot
2016-01-14 Simon HuberBugfix in compU and compGlue commit | commitdiff | tree | snapshot
2016-01-12 Simon HuberBugfix by Fabian Ruch commit | commitdiff | tree | snapshot
2016-01-09 Anders Mörtbergfix bug commit | commitdiff | tree | snapshot
2016-01-08 Anders Mörtbergcleaning commit | commitdiff | tree | snapshot
2016-01-07 Anders Mörtbergcomment gradLemmaU commit | commitdiff | tree | snapshot
2016-01-07 Anders Mörtbergremove @@@ commit | commitdiff | tree | snapshot
2016-01-07 Anders Mörtbergdont write to a file commit | commitdiff | tree | snapshot
2016-01-07 Anders Mörtberg"_" in constPath again commit | commitdiff | tree | snapshot
2016-01-05 Anders Mörtberguse compConstLine commit | commitdiff | tree | snapshot
2016-01-05 Anders Mörtbergadd the huge normal form of corrUniv which trigger... commit | commitdiff | tree | snapshot
2016-01-05 Anders Mörtbergremove a space in a comment commit | commitdiff | tree | snapshot
2016-01-05 Anders Mörtbergchange constPath to avoid strange bug commit | commitdiff | tree | snapshot
2016-01-05 Anders Mörtbergcomment commit | commitdiff | tree | snapshot
2016-01-05 Anders Mörtbergadd parsing of ! in beginning of idents commit | commitdiff | tree | snapshot
2016-01-05 Anders Mörtbergremove all <_> commit | commitdiff | tree | snapshot
2016-01-05 Anders Mörtbergchange printing of compU commit | commitdiff | tree | snapshot
2016-01-04 coquandadded an example with ordinals commit | commitdiff | tree | snapshot
2016-01-04 Anders MörtbergMore cleaning commit | commitdiff | tree | snapshot
2016-01-04 Anders MörtbergAdd bool example to univalence.ctt commit | commitdiff | tree | snapshot
2016-01-04 Anders MörtbergCleaning and removal of duplicate code. Put all proofs... commit | commitdiff | tree | snapshot
2016-01-04 Anders MörtbergRefactoring and move old code on equivalences to experi... commit | commitdiff | tree | snapshot
next
My fork of cubicaltt with web interface using Reflex.