git.ak3n.com - cubicaltt.git/shortlog

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-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
2015-12-15	Simon Huber	Bugfix for type checking glueElems by Fabian Ruch	commit \| commitdiff \| tree \| snapshot
2015-12-14	Simon Huber	Efficient @@ for fresh names	commit \| commitdiff \| tree \| snapshot
2015-12-14	Simon Huber	Simplified pathComp	commit \| commitdiff \| tree \| snapshot
2015-12-11	Anders Mörtberg	start working on hz	commit \| commitdiff \| tree \| snapshot
2015-12-11	Anders Mörtberg	Clean setquot	commit \| commitdiff \| tree \| snapshot
2015-12-09	Anders Mörtberg	add IdPathTest1	commit \| commitdiff \| tree \| snapshot
2015-12-04	Anders Mörtberg	minor modification to foo	commit \| commitdiff \| tree \| snapshot
2015-12-04	Anders Mörtberg	another small test	commit \| commitdiff \| tree \| snapshot
2015-12-04	Anders Mörtberg	change es' to es, not sure if this is correct...	commit \| commitdiff \| tree \| snapshot
2015-12-04	Anders Mörtberg	Simpler version of gradlemmaU	commit \| commitdiff \| tree \| snapshot
2015-12-04	Anders Mörtberg	minor changes	commit \| commitdiff \| tree \| snapshot
2015-12-04	Anders Mörtberg	Add the missing line in comp!	commit \| commitdiff \| tree \| snapshot
2015-12-04	Anders Mörtberg	another example	commit \| commitdiff \| tree \| snapshot
2015-12-04	Anders Mörtberg	remove reglarity	commit \| commitdiff \| tree \| snapshot
2015-12-04	Anders Mörtberg	add a shrink function that can be used to not print...	commit \| commitdiff \| tree \| snapshot
2015-12-04	Anders Mörtberg	Add VCompU to normal and conv	commit \| commitdiff \| tree \| snapshot
2015-12-04	Anders Mörtberg	Add some test of normal forms	commit \| commitdiff \| tree \| snapshot
2015-12-04	Anders Mörtberg	Reintroduce compU	commit \| commitdiff \| tree \| snapshot
2015-12-03	Anders Mörtberg	add a short version of setquot	commit \| commitdiff \| tree \| snapshot
2015-12-02	Anders Mörtberg	Prove direct version of uahp	commit \| commitdiff \| tree \| snapshot
2015-12-02	Anders Mörtberg	fix comment	commit \| commitdiff \| tree \| snapshot
2015-12-02	Anders Mörtberg	Cleaning	commit \| commitdiff \| tree \| snapshot
2015-12-02	Anders Mörtberg	finish setquot example	commit \| commitdiff \| tree \| snapshot
2015-12-02	Anders Mörtberg	prove that bool is a set	commit \| commitdiff \| tree \| snapshot
2015-12-02	Anders Mörtberg	prove that hProp is a set	commit \| commitdiff \| tree \| snapshot
2015-12-02	Anders Mörtberg	prove uahp	commit \| commitdiff \| tree \| snapshot
2015-12-01	Anders Mörtberg	setquot	commit \| commitdiff \| tree \| snapshot
2015-11-26	Simon Huber	Another formulation of univalence	commit \| commitdiff \| tree \| snapshot
2015-11-19	Anders Mörtberg	indentation	commit \| commitdiff \| tree \| snapshot
next

My fork of cubicaltt with web interface using Reflex.

RSS Atom