git.ak3n.com - cubicaltt.git/shortlog

2015-06-18	Anders	Reintroduce transport	commit \| commitdiff \| tree \| snapshot
2015-06-18	Anders	Reintroduce glueElem	commit \| commitdiff \| tree \| snapshot
2015-06-17	Anders	Finish the proof of univalence	commit \| commitdiff \| tree \| snapshot
2015-06-17	Anders Mörtberg	Start adding gradlemma to finish proof of univalence	commit \| commitdiff \| tree \| snapshot
2015-06-16	Simon Huber	A proof of univalence (wip)	commit \| commitdiff \| tree \| snapshot
2015-06-16	Simon Huber	Adds projections for equivs	commit \| commitdiff \| tree \| snapshot
2015-06-16	Simon Huber	Typo	commit \| commitdiff \| tree \| snapshot
2015-06-16	Simon Huber	Don't require equivalences to be eta-expanded	commit \| commitdiff \| tree \| snapshot
2015-06-15	Simon Huber	Finished eqToEquiv	commit \| commitdiff \| tree \| snapshot
2015-06-09	Simon Huber	Rename hiso to equiv	commit \| commitdiff \| tree \| snapshot
2015-06-09	Simon Huber	Equivalences instead of isos (wip)	commit \| commitdiff \| tree \| snapshot
2015-06-08	Anders	Make bool, circle and integer compile	commit \| commitdiff \| tree \| snapshot
2015-06-08	Anders	Add lemSimpl	commit \| commitdiff \| tree \| snapshot
2015-06-08	Simon Huber	Convertability for hComp	commit \| commitdiff \| tree \| snapshot
2015-06-06	Anders Mörtberg	Update aim.ctt again	commit \| commitdiff \| tree \| snapshot
2015-06-06	Anders Mörtberg	Update aim.ctt	commit \| commitdiff \| tree \| snapshot
2015-06-06	Anders Mörtberg	Add AIM talk	commit \| commitdiff \| tree \| snapshot
2015-06-05	Simon Huber	Less definitional equalities for glue	commit \| commitdiff \| tree \| snapshot
2015-06-05	Simon Huber	Throw out transport	commit \| commitdiff \| tree \| snapshot
2015-06-05	Simon Huber	Merge branch 'hisoproj' into no_regular	commit \| commitdiff \| tree \| snapshot
2015-06-05	Simon Huber	Finished eqToIso and removed constants for comp in U	commit \| commitdiff \| tree \| snapshot
2015-06-04	Anders Mörtberg	Update squeezeHIT	commit \| commitdiff \| tree \| snapshot
2015-06-04	Simon Huber	Equality to isomorphism (wip)	commit \| commitdiff \| tree \| snapshot
2015-06-04	Anders Mörtberg	define trans in terms of gencomp	commit \| commitdiff \| tree \| snapshot
2015-06-04	Simon Huber	Added fill as a term and comp is now genComp	commit \| commitdiff \| tree \| snapshot
2015-06-04	Anders	Add genComp and some examples for debugging	commit \| commitdiff \| tree \| snapshot
2015-06-04	Anders	remove commented code	commit \| commitdiff \| tree \| snapshot
2015-06-04	Simon Huber	Adapted HITs	commit \| commitdiff \| tree \| snapshot
2015-06-04	Simon Huber	Fix for neutral unglues	commit \| commitdiff \| tree \| snapshot
2015-06-04	Simon Huber	Added neutral values for unglue	commit \| commitdiff \| tree \| snapshot
2015-06-04	Simon Huber	Adapted	commit \| commitdiff \| tree \| snapshot
2015-06-04	Simon Huber	Added constructor for comp in U	commit \| commitdiff \| tree \| snapshot
2015-06-03	Simon Huber	Fix use of compLine	commit \| commitdiff \| tree \| snapshot
2015-06-03	Anders Mörtberg	Fix add_comm	commit \| commitdiff \| tree \| snapshot
2015-06-03	Anders	isNeutralComp, small fixes to comp and comment things...	commit \| commitdiff \| tree \| snapshot
2015-06-03	Simon Huber	Adapted prelude	commit \| commitdiff \| tree \| snapshot
2015-06-03	Simon Huber	Finished first version	commit \| commitdiff \| tree \| snapshot
2015-06-03	Simon Huber	Adapted compGlue	commit \| commitdiff \| tree \| snapshot
2015-06-02	Simon Huber	Started adapting for the non-regular setting (wip)	commit \| commitdiff \| tree \| snapshot
2015-05-18	Anders	Add direct proof that s2 is trivial (for the HIT defini...	commit \| commitdiff \| tree \| snapshot
2015-05-16	coquand	simple examples on nat and list	commit \| commitdiff \| tree \| snapshot
2015-05-12	Anders	Isomorphism of the direct and the susp definition of S2	commit \| commitdiff \| tree \| snapshot
2015-05-11	Anders	Fix the bug in transport and add optimizations to compE...	commit \| commitdiff \| tree \| snapshot
2015-05-08	Anders	Add exchange law and genPiS3	commit \| commitdiff \| tree \| snapshot
2015-05-08	Anders	Change order in checkPathSystem	commit \| commitdiff \| tree \| snapshot
2015-05-06	Anders	Add check that systems don't contain the same face...	commit \| commitdiff \| tree \| snapshot
2015-05-06	Anders	The loop space of the torus is equal to Z * Z	commit \| commitdiff \| tree \| snapshot
2015-05-06	Anders	Cleaning	commit \| commitdiff \| tree \| snapshot
2015-05-06	Anders	Clean helix	commit \| commitdiff \| tree \| snapshot
2015-05-06	Anders	More efficient implementation of environments	commit \| commitdiff \| tree \| snapshot
2015-05-05	Anders Mörtberg	Comment the two slowest tests in mystery	commit \| commitdiff \| tree \| snapshot
2015-05-05	Anders Mörtberg	Add optimization to act	commit \| commitdiff \| tree \| snapshot
2015-05-05	Anders Mörtberg	Add new proof that loopS1 is a set	commit \| commitdiff \| tree \| snapshot
2015-05-05	mortberg	Merge pull request #10 from dlicata335/master	commit \| commitdiff \| tree \| snapshot
2015-05-05	Dan Licata	cleaned up mystery.ctt for inclusion in repository...	commit \| commitdiff \| tree \| snapshot
2015-05-05	Anders Mörtberg	Swap test2 and test3 to correspond to what is in cubical	commit \| commitdiff \| tree \| snapshot
2015-05-05	Anders Mörtberg	Add fix to comp for sums	commit \| commitdiff \| tree \| snapshot
2015-05-04	Anders Mörtberg	Add pi4s3 until test0To5	commit \| commitdiff \| tree \| snapshot
2015-05-04	Anders Mörtberg	Add -t flag	commit \| commitdiff \| tree \| snapshot
2015-05-04	Simon Huber	nicer error msg	commit \| commitdiff \| tree \| snapshot
2015-05-04	Simon Huber	fixed printing of glueLine	commit \| commitdiff \| tree \| snapshot
2015-05-04	Simon Huber	move neutrality test in app of a split to a composition	commit \| commitdiff \| tree \| snapshot
2015-05-04	Simon Huber	use unqualified mapWithKey	commit \| commitdiff \| tree \| snapshot
2015-05-03	Anders Mörtberg	Add missing spaces	commit \| commitdiff \| tree \| snapshot
2015-05-03	mortberg	Merge pull request #9 from dlicata335/master	commit \| commitdiff \| tree \| snapshot
2015-05-02	Dan Licata	six is not the successor of six	commit \| commitdiff \| tree \| snapshot
2015-05-02	Dan Licata	mystery example: beta reduce some compIds	commit \| commitdiff \| tree \| snapshot
2015-05-02	Dan Licata	compile with -rtsopts so you can set the stack space	commit \| commitdiff \| tree \| snapshot
2015-05-02	Dan Licata	use synthetic homotopy theory to get a function on...	commit \| commitdiff \| tree \| snapshot
2015-05-02	Dan Licata	use synthetic homotopy theory to get a function on...	commit \| commitdiff \| tree \| snapshot
2015-05-01	Dan Licata	torus = two circles proof cleanup	commit \| commitdiff \| tree \| snapshot
2015-05-01	Dan Licata	torus = two circles proof	commit \| commitdiff \| tree \| snapshot
2015-04-30	Simon Huber	add more parentheses	commit \| commitdiff \| tree \| snapshot
2015-04-30	Simon Huber	non-trivial homotopy in the loop space of stwo	commit \| commitdiff \| tree \| snapshot
2015-04-30	Simon Huber	allow overshadowing of names	commit \| commitdiff \| tree \| snapshot
2015-04-30	coquand	updated collection	commit \| commitdiff \| tree \| snapshot
2015-04-30	coquand	updated setTrunc	commit \| commitdiff \| tree \| snapshot
2015-04-30	coquand	added some test for pi1S2	commit \| commitdiff \| tree \| snapshot
2015-04-30	coquand	pi1S2 is trivial	commit \| commitdiff \| tree \| snapshot
2015-04-30	coquand	piS2 is trivial	commit \| commitdiff \| tree \| snapshot
2015-04-30	coquand	univalence	commit \| commitdiff \| tree \| snapshot
2015-04-30	coquand	the collection of sets is a groupoid	commit \| commitdiff \| tree \| snapshot
2015-04-29	Simon Huber	added glueLine (wip)	commit \| commitdiff \| tree \| snapshot
2015-04-29	Simon Huber	improve error message	commit \| commitdiff \| tree \| snapshot
2015-04-29	coquand	added hopf fibration	commit \| commitdiff \| tree \| snapshot
2015-04-29	coquand	more efficient version of groupoid truncation	commit \| commitdiff \| tree \| snapshot
2015-04-28	coquand	nicer proof of lemtransport	commit \| commitdiff \| tree \| snapshot
2015-04-28	coquand	an example of normal form	commit \| commitdiff \| tree \| snapshot
2015-04-28	coquand	added groupoid truncation	commit \| commitdiff \| tree \| snapshot
2015-04-28	coquand	added pi1s2	commit \| commitdiff \| tree \| snapshot
2015-04-27	coquand	clean mult	commit \| commitdiff \| tree \| snapshot
2015-04-27	coquand	added some examples for pi1S2	commit \| commitdiff \| tree \| snapshot
2015-04-23	Anders	Add the test of parsing output from integer back	commit \| commitdiff \| tree \| snapshot
2015-04-23	Anders	Fix set	commit \| commitdiff \| tree \| snapshot
2015-04-23	Anders	Normalize formulas	commit \| commitdiff \| tree \| snapshot
2015-04-23	Anders	Fix dnf	commit \| commitdiff \| tree \| snapshot
2015-04-23	Anders	Elimination principle for set truncation	commit \| commitdiff \| tree \| snapshot
2015-04-23	Simon Huber	bugix: take the border of the system where is=js	commit \| commitdiff \| tree \| snapshot
2015-04-21	Anders Mörtberg	Refactoring of examples	commit \| commitdiff \| tree \| snapshot
2015-04-21	Anders	Add normalization of environments	commit \| commitdiff \| tree \| snapshot
next

My fork of cubicaltt with web interface using Reflex.

RSS Atom