cubicaltt.git
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
2015-04-21 coquandproof that mult is an equivalence
2015-04-21 coquandproof that mult is an equivalence
2015-04-21 coquandupdated proofs of Hedberg's Theorem
2015-04-21 AndersImprove printing of lambdas and paths
2015-04-21 AndersMake conversion use a list of names instead
2015-04-21 AndersRemove unnecessary argument to addBranch
2015-04-21 AndersRemove unnecessary monadic code in Typechecker (no...
2015-04-21 Anders MörtbergChange ? to !
2015-04-21 Anders MörtbergFix examples
2015-04-21 Anders MörtbergUpdate graph script
2015-04-21 Anders MörtbergAdd testall
2015-04-21 Anders MörtbergFix helix
2015-04-21 Anders MörtbergFix newhedberg
2015-04-21 Anders MörtbergUse old gensym and fresh again
2015-04-20 Anders MörtbergFix printing of VPi
2015-04-20 Anders MörtbergFix retract
2015-04-20 AndersMake normal print nicer names
2015-04-20 AndersFix printing of @
2015-04-20 AndersAdd quotient example
2015-04-20 AndersSplit higherhit into multiple files
2015-04-20 AndersMerge remote-tracking branch 'origin/higherhits'
2015-04-20 Anders MörtbergFix the way @ binds (it is now like normal application)
2015-04-20 Anders MörtbergFix a TODO in the resolver (the arguments in a path...
2015-04-20 Anders MörtbergFix all the old examples of HITs
2015-04-20 Anders MörtbergRemove the @ in PLabel
2015-04-19 coquandany isomorphism is an equivalence
2015-04-19 coquandif A and B are isomorphic, set A -> set B, normal form
2015-04-19 coquandif A and B are isomorphic, prop A -> prop B, normal...
2015-04-19 coquandresult on equivalence of fibers
2015-04-19 coquandnew proof of Hedberg's theorem
2015-04-18 Simon Hubersome examples
2015-04-18 Simon HuberlookName error msg for debugging
2015-04-18 Simon Huberbugfix in PBranches
2015-04-18 Simon Huberlet the system in a pcon know about all pcons in the sum
2015-04-18 Simon Huberbugfix
2015-04-18 Simon Huberbugfix in resolver
2015-04-18 Simon Huberwip (not working yet)
2015-04-17 AndersFix printing of goals and environments (TODO: Fix ...
2015-04-17 AndersRewrite app and support using case-of
2015-04-17 AndersUse Except instead or Error
2015-04-17 AndersRemove tabs
2015-04-17 Anders MörtbergOnly show second part of VPi x (VLam ...)
2015-04-17 Anders MörtbergAlso normalize the type of lambdas and print VPi nicer
2015-04-17 Anders MörtbergUse showTer1 to print closures
2015-04-17 Anders MörtbergFix uafunext2
2015-04-16 AndersRemove some incidentally commited holes
2015-04-16 AndersReintroduce _ in identifier again
2015-04-16 Simon Huberreintroduce nicer mkVar
2015-04-16 Simon Huberkeep name if we have it when generating a fresh name
2015-04-16 Simon Huberchange mkVar back to how it was
2015-04-16 Anders MörtbergAdd indentation to Checking and start changing mkVar...
2015-04-16 Anders MörtbergOnly print File loaded if file type checks
2015-04-16 Anders MörtbergChange gensym
2015-04-16 Anders MörtbergMake holes print the context
2015-04-16 Anders MörtbergTrailing whitespace
2015-04-16 Anders MörtbergFix undefined
2015-04-15 AndersFinish example of integers as a HIT
2015-04-15 AndersRemove some code from ex1
2015-04-15 AndersFix bug in type checker for HITs
2015-04-15 AndersFix undefined
2015-04-15 Anders MörtbergRemove VUndef
2015-04-15 Anders MörtbergAdd very simple support for holes
2015-04-14 Anders MörtbergMake list compile
2015-04-14 Anders MörtbergMake undefined only occur as a declaration so that...
2015-04-14 Anders MörtbergUndef is neutral (but there is an issue with inferType...
2015-04-14 Anders MörtbergStart defining integers as a HIT and proving that they...
2015-04-14 AndersFix printing of fst, snd and lambdas
2015-04-14 AndersUpdate the description in demo.ctt
2015-04-14 coquandadded some lines in ex1.ctt
2015-04-14 coquandadded some lines in ex1.ctt
2015-04-14 coquandsmall change in helix.ctt
2015-04-14 coquandone example with constant functions
2015-04-13 Anders MörtbergFix bug in Resolver
2015-04-13 Anders MörtbergRemove contr from equiv
2015-04-13 Simon Huberlicense should include names
2015-04-13 coquandsmall modification in the file susp
2015-04-13 Anders MörtbergUpdate help message
2015-04-13 Anders MörtbergUpdate README
next