git.ak3n.com - cubicaltt.git/shortlog

2016-07-05	Anders Mörtberg	wip	commit \| commitdiff \| tree \| snapshot
2016-07-05	Anders Mörtberg	wip on an equivalent presentation of the circle as...	commit \| commitdiff \| tree \| snapshot
2016-07-05	Anders Mörtberg	minor changes to circle	commit \| commitdiff \| tree \| snapshot
2016-07-01	Simon Huber	Merge pull request #39 from abooij/prop-trunc	commit \| commitdiff \| tree \| snapshot
2016-06-02	Auke Booij	Add warning about recursive HITs	commit \| commitdiff \| tree \| snapshot
2016-06-02	Auke Booij	Rename truncP to inh	commit \| commitdiff \| tree \| snapshot
2016-06-01	Auke Booij	implement propositional truncation	commit \| commitdiff \| tree \| snapshot
2016-05-24	Anders Mörtberg	add reserved keywords to README	commit \| commitdiff \| tree \| snapshot
2016-04-27	Thierry Coquand	small change	commit \| commitdiff \| tree \| snapshot
2016-04-27	Thierry Coquand	we should improve the evaluator	commit \| commitdiff \| tree \| snapshot
2016-04-14	Anders Mörtberg	Finish binnat example and add elimination principles...	commit \| commitdiff \| tree \| snapshot
2016-04-12	Anders Mörtberg	Start porting binnat	commit \| commitdiff \| tree \| snapshot
2016-04-08	Thierry Coquand	other proof of lemPropF	commit \| commitdiff \| tree \| snapshot
2016-04-02	Thierry Coquand	some computations	commit \| commitdiff \| tree \| snapshot
2016-04-01	Thierry Coquand	study of multiplication on S1	commit \| commitdiff \| tree \| snapshot
2016-04-01	Thierry Coquand	proof that S1 is a groupoid	commit \| commitdiff \| tree \| snapshot
2016-03-06	Anders Mörtberg	Merge pull request #36 from georgydunaev/master	commit \| commitdiff \| tree \| snapshot
2016-03-06	Georgy Dunaev	added imports and changed collection.ctt (corrUniv...	commit \| commitdiff \| tree \| snapshot
2016-03-03	Simon Huber	Fix squeezeHIT for non-recursive HITs	commit \| commitdiff \| tree \| snapshot
2016-03-03	Simon Huber	Anders bugfix for squeezes	commit \| commitdiff \| tree \| snapshot
2016-02-18	Anders Mörtberg	Merge pull request #29 from abooij/master	commit \| commitdiff \| tree \| snapshot
2016-02-17	Auke Booij	Soften version constraints	commit \| commitdiff \| tree \| snapshot
2016-02-11	Simon Huber	Fix printing of environments	commit \| commitdiff \| tree \| snapshot
2016-02-10	Simon Huber	Test for correct length in checks (Fixes #27)	commit \| commitdiff \| tree \| snapshot
2016-01-27	Anders Mörtberg	add a small test of the grad lemma	commit \| commitdiff \| tree \| snapshot
2016-01-23	Anders Mörtberg	cleaning	commit \| commitdiff \| tree \| snapshot
2016-01-23	Anders Mörtberg	Merge branch 'nunivalence'	commit \| commitdiff \| tree \| snapshot
2016-01-23	Anders Mörtberg	comment in nthmUniv	commit \| commitdiff \| tree \| snapshot
2016-01-23	Anders Mörtberg	add the correct normal form of univalence	commit \| commitdiff \| tree \| snapshot
2016-01-23	Anders Mörtberg	use uahp' in setquot instead	commit \| commitdiff \| tree \| snapshot
2016-01-20	Anders Mörtberg	Fix ö	commit \| commitdiff \| tree \| snapshot
2016-01-20	Simon Huber	Updated readme	commit \| commitdiff \| tree \| snapshot
2016-01-18	Simon Huber	Missing case for checking GlueElem against VCompU	commit \| commitdiff \| tree \| snapshot
2016-01-15	Anders Mörtberg	move two lemmas to nat	commit \| commitdiff \| tree \| snapshot
2016-01-15	Anders Mörtberg	finish the hz exercise	commit \| commitdiff \| tree \| snapshot
2016-01-15	Anders Mörtberg	Finish 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 Huber	Bugfix in inferType	commit \| commitdiff \| tree \| snapshot
2016-01-15	Anders Mörtberg	setquot is a set	commit \| commitdiff \| tree \| snapshot
2016-01-15	Anders Mörtberg	one less undefined	commit \| commitdiff \| tree \| snapshot
2016-01-15	Anders Mörtberg	squash some admits	commit \| commitdiff \| tree \| snapshot
2016-01-14	Anders Mörtberg	minor changes	commit \| commitdiff \| tree \| snapshot
2016-01-14	Anders Mörtberg	more on setquot. on the way to define an equality test...	commit \| commitdiff \| tree \| snapshot
2016-01-14	Anders Mörtberg	add nlem1	commit \| commitdiff \| tree \| snapshot
2016-01-14	Anders Mörtberg	Change printing of environments	commit \| commitdiff \| tree \| snapshot
2016-01-14	Anders Mörtberg	rename sig to Sigma and make setquot compile	commit \| commitdiff \| tree \| snapshot
2016-01-14	Anders Mörtberg	make bool compile and move tests using univalence for...	commit \| commitdiff \| tree \| snapshot
2016-01-14	Simon Huber	Bugfix in compU and compGlue	commit \| commitdiff \| tree \| snapshot
2016-01-12	Simon Huber	Bugfix by Fabian Ruch	commit \| commitdiff \| tree \| snapshot
2016-01-09	Anders Mörtberg	fix bug	commit \| commitdiff \| tree \| snapshot
2016-01-08	Anders Mörtberg	cleaning	commit \| commitdiff \| tree \| snapshot
2016-01-07	Anders Mörtberg	comment gradLemmaU	commit \| commitdiff \| tree \| snapshot
2016-01-07	Anders Mörtberg	remove @@@	commit \| commitdiff \| tree \| snapshot
2016-01-07	Anders Mörtberg	dont 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örtberg	use compConstLine	commit \| commitdiff \| tree \| snapshot
2016-01-05	Anders Mörtberg	add the huge normal form of corrUniv which trigger...	commit \| commitdiff \| tree \| snapshot
2016-01-05	Anders Mörtberg	remove a space in a comment	commit \| commitdiff \| tree \| snapshot
2016-01-05	Anders Mörtberg	change constPath to avoid strange bug	commit \| commitdiff \| tree \| snapshot
2016-01-05	Anders Mörtberg	comment	commit \| commitdiff \| tree \| snapshot
2016-01-05	Anders Mörtberg	add parsing of ! in beginning of idents	commit \| commitdiff \| tree \| snapshot
2016-01-05	Anders Mörtberg	remove all <_>	commit \| commitdiff \| tree \| snapshot
2016-01-05	Anders Mörtberg	change printing of compU	commit \| commitdiff \| tree \| snapshot
2016-01-04	coquand	added an example with ordinals	commit \| commitdiff \| tree \| snapshot
2016-01-04	Anders Mörtberg	More cleaning	commit \| commitdiff \| tree \| snapshot
2016-01-04	Anders Mörtberg	Add bool example to univalence.ctt	commit \| commitdiff \| tree \| snapshot
2016-01-04	Anders Mörtberg	Cleaning and removal of duplicate code. Put all proofs...	commit \| commitdiff \| tree \| snapshot
2016-01-04	Anders Mörtberg	Refactoring and move old code on equivalences to experi...	commit \| commitdiff \| tree \| snapshot
2015-12-31	Anders Mörtberg	Make aim.ctt compile	commit \| commitdiff \| tree \| snapshot
2015-12-31	Anders Mörtberg	Merge branch 'compU'	commit \| commitdiff \| tree \| snapshot
2015-12-31	Anders Mörtberg	Merge branch 'testUniv'	commit \| commitdiff \| tree \| snapshot
2015-12-31	Anders Mörtberg	update aim.ctt	commit \| commitdiff \| tree \| snapshot
2015-12-30	Anders Mörtberg	add standard formulation of univalence	commit \| commitdiff \| tree \| snapshot
2015-12-30	coquand	an example of normal form	commit \| commitdiff \| tree \| snapshot
2015-12-29	coquand	updated collection	commit \| commitdiff \| tree \| snapshot
2015-12-29	coquand	small change	commit \| commitdiff \| tree \| snapshot
2015-12-29	coquand	updated sigma, not use of J	commit \| commitdiff \| tree \| snapshot
2015-12-29	coquand	updated multS1	commit \| commitdiff \| tree \| snapshot
2015-12-29	coquand	circle now works with this version of univalence	commit \| commitdiff \| tree \| snapshot
2015-12-27	coquand	changed compU	commit \| commitdiff \| tree \| snapshot
2015-12-27	coquand	simple tests for univalence	commit \| commitdiff \| tree \| snapshot
2015-12-27	coquand	neutral for compU	commit \| commitdiff \| tree \| snapshot
2015-12-26	coquand	Makefile	commit \| commitdiff \| tree \| snapshot
2015-12-26	coquand	other proof of univalence	commit \| commitdiff \| tree \| snapshot
2015-12-26	coquand	corrected Eval	commit \| commitdiff \| tree \| snapshot
2015-12-26	coquand	an example where we type-checked a normal form	commit \| commitdiff \| tree \| snapshot
2015-12-26	coquand	proof of univalence?	commit \| commitdiff \| tree \| snapshot
2015-12-26	coquand	univalence	commit \| commitdiff \| tree \| snapshot
2015-12-26	coquand	proof of univalence	commit \| commitdiff \| tree \| snapshot
2015-12-26	coquand	updated testContr	commit \| commitdiff \| tree \| snapshot
2015-12-22	coquand	some lemmas about contractible types	commit \| commitdiff \| tree \| snapshot
2015-12-19	coquand	testEquiv	commit \| commitdiff \| tree \| snapshot
2015-12-19	coquand	simplified transIdFun	commit \| commitdiff \| tree \| snapshot
2015-12-19	coquand	simpler version of idToId in testEquiv	commit \| commitdiff \| tree \| snapshot
2015-12-19	coquand	testEquiv	commit \| commitdiff \| tree \| snapshot
2015-12-19	coquand	simplified transIdFun	commit \| commitdiff \| tree \| snapshot
2015-12-18	coquand	simpler version of idToId in testEquiv	commit \| commitdiff \| tree \| snapshot
2015-12-18	Anders Mörtberg	alternative definition of equivalences	commit \| commitdiff \| tree \| snapshot
2015-12-17	Simon Huber	Fixed eqToEquiv	commit \| commitdiff \| tree \| snapshot
2015-12-16	Simon Huber	Switched back to equiv, simplified glue	commit \| commitdiff \| tree \| snapshot
next

My fork of cubicaltt with web interface using Reflex.

RSS Atom