git.ak3n.com - cubicaltt.git/shortlog

2016-07-07	Rafaël Bocquet	Speed up conv	commit \| commitdiff \| tree \| snapshot
2016-07-07	Rafaël Bocquet	add some comments in category.ctt and csystem.ctt	commit \| commitdiff \| tree \| snapshot
2016-06-20	Rafaël Bocquet	Two equivalent categories are equal	commit \| commitdiff \| tree \| snapshot
2016-06-14	Rafaël Bocquet	wip	commit \| commitdiff \| tree \| snapshot
2016-06-13	Rafaël Bocquet	wip	commit \| commitdiff \| tree \| snapshot
2016-05-31	Rafaël Bocquet	Split csystem.ctt into category.ctt and csystem.ctt	commit \| commitdiff \| tree \| snapshot
2016-05-23	Rafaël Bocquet	Construction of a C0-System from a universe category	commit \| commitdiff \| tree \| snapshot
2016-05-23	Rafaël Bocquet	Fix the module name	commit \| commitdiff \| tree \| snapshot
2016-05-23	Rafaël Bocquet	(wip) construction of a C0-System from a universe category	commit \| commitdiff \| tree \| snapshot
2016-05-10	Rafaël Bocquet	Both definitions of C systems; the second one implies...	commit \| commitdiff \| tree \| snapshot
2016-04-21	Rafaël Bocquet	Merge branch 'master' of github.com:mortberg/cubicaltt...	commit \| commitdiff \| tree \| snapshot
2016-04-21	Rafaël Bocquet	definition of C systems	commit \| commitdiff \| tree \| snapshot
2016-04-14	Anders Mörtberg	Finish binnat example and add elimination principles...	commit \| commitdiff \| tree \| snapshot
2016-04-14	Rafaël Bocquet	simple computation using multZ	commit \| commitdiff \| tree \| snapshot
2016-04-14	Rafaël Bocquet	torsor multiplication	commit \| commitdiff \| tree \| snapshot
2016-04-13	Rafaël Bocquet	eval ignores opaqueness	commit \| commitdiff \| tree \| snapshot
2016-04-12	Anders Mörtberg	Start porting binnat	commit \| commitdiff \| tree \| snapshot
2016-04-12	Rafaël Bocquet	visible_all command	commit \| commitdiff \| tree \| snapshot
2016-04-12	Rafaël Bocquet	Opaque/Visible definitions	commit \| commitdiff \| tree \| snapshot
2016-04-08	Rafaël Bocquet	some proofs	commit \| commitdiff \| tree \| snapshot
2016-04-08	Rafaël Bocquet	slow proof	commit \| commitdiff \| tree \| snapshot
2016-04-08	Thierry Coquand	other proof of lemPropF	commit \| commitdiff \| tree \| snapshot
2016-04-07	Rafaël Bocquet	Only ZEquiv : isEquiv (plus x) is not proven	commit \| commitdiff \| tree \| snapshot
2016-04-06	Rafaël Bocquet	S1 = BZ	commit \| commitdiff \| tree \| snapshot
2016-04-05	Rafaël Bocquet	Merge branch 'master' of https://github.com/mortberg...	commit \| commitdiff \| tree \| snapshot
2016-04-05	Rafaël Bocquet	Z = Id BZ ZBZ ZBZ	commit \| commitdiff \| tree \| snapshot
2016-04-04	Rafaël Bocquet	.	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
next

My fork of cubicaltt with web interface using Reflex.

RSS Atom