git.ak3n.com - cubicaltt.git/shortlog

2015-07-02	Anders Mörtberg	Add the proof of univalence using glue with isos	commit \| commitdiff \| tree \| snapshot
2015-07-01	Anders Mörtberg	Fix imports	commit \| commitdiff \| tree \| snapshot
2015-06-30	Anders Mörtberg	Fix typo in typechecker and redefine isoId using glue	commit \| commitdiff \| tree \| snapshot
2015-06-30	Anders Mörtberg	Revert to using iso instead of equiv	commit \| commitdiff \| tree \| snapshot
2015-06-29	Anders	Some lemmas about equivs	commit \| commitdiff \| tree \| snapshot
2015-06-29	Anders	Update aim talk	commit \| commitdiff \| tree \| snapshot
2015-06-28	Simon Huber	Fixed lemCompInv	commit \| commitdiff \| tree \| snapshot
2015-06-24	Simon Huber	Equations for subst and J	commit \| commitdiff \| tree \| snapshot
2015-06-22	Simon Huber	Fix typo in inferType	commit \| commitdiff \| tree \| snapshot
2015-06-18	Anders	Restate univalence	commit \| commitdiff \| tree \| snapshot
2015-06-18	Anders	Update susp	commit \| commitdiff \| tree \| snapshot
2015-06-18	Anders	Update README and update demo.ctt	commit \| commitdiff \| tree \| snapshot
2015-06-18	Anders	Cleaning and reorganization of files	commit \| commitdiff \| tree \| snapshot
2015-06-18	Anders	Merge branch 'no_regular' into equiv	commit \| commitdiff \| tree \| snapshot
2015-06-18	Anders	Cleaning	commit \| commitdiff \| tree \| snapshot
2015-06-18	Anders	Add typechecking for glueElem	commit \| commitdiff \| tree \| snapshot
2015-06-18	Anders	Remove old code for eqToIso and gradLemma for isos	commit \| commitdiff \| tree \| snapshot
2015-06-18	Anders	Make more names unqualified when importing Map and...	commit \| commitdiff \| tree \| snapshot
2015-06-18	Anders	Improve printing of fst and snd	commit \| commitdiff \| tree \| snapshot
2015-06-18	Anders	Remove commented code for GlueLine, GlueLineElem, CompE...	commit \| commitdiff \| tree \| snapshot
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-15	Simon Huber	Fix handling of neutral for composition in sums	commit \| commitdiff \| tree \| snapshot
2015-06-13	Anders	Fix hisos''	commit \| commitdiff \| tree \| snapshot
2015-06-12	Anders	Fix printing	commit \| commitdiff \| tree \| snapshot
2015-06-10	Simon Huber	Convertability for HSum	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
next

My fork of cubicaltt with web interface using Reflex.

RSS Atom