~helmut/bidiragda.git - Bidirectionalization for Free in Agda (http://subdivi.de/~helmut/academia/fsbxia.pdf)

Age	Commit message (Collapse)	Author
2014-02-26	convert LiftGet module to using heterogeneous equality	Helmut Grohne
	The reduction in proof length is impressive.
2014-02-03	also show the other direction GetL-to-GetV	Helmut Grohne

2014-02-03	add a GetV-to-GetL transformer	Helmut Grohne
	This is an improved version of getVec-to-getList in that it also transports the corresponding free theorem.
2014-01-30	pass get functions as records	Helmut Grohne
	This allows passing both getlen and get as a single parameter. It also allows to make the free theorem a prerequisite instead of a postulate.
2013-12-16	move generic functions to a new Generic module	Helmut Grohne

2012-10-05	move all postulates to one module	Helmut Grohne
	This should make it easier to see what is assumed.
2012-09-27	remove getVec-getlen in favour of plain subst	Helmut Grohne

2012-09-27	move definition of get-type to BFF and use it everywhere	Helmut Grohne

2012-09-14	\::-subst is a special case of subst-cong	Helmut Grohne

2012-09-14	vec-len-via-list and length-toList are the same	Helmut Grohne

2012-09-14	complete missing parts of LiftGet	Helmut Grohne
	Thanks to Joachim Breitner and Wouter Swierstra for their encouragement and hints. Note that the result duplicates work at this point, but the proofs are complete.
2012-09-11	show fromList-toList in the subst form	Helmut Grohne
	Thanks to Joachim Breitner for assisting and pointing to proof-irrelevance.
2012-09-11	LiftGet: replace vec-length-same with toList-subst	Helmut Grohne
	The name vec-length-same hides the fact that it eliminates a toList and a fromList. Actually a more generic form without fromList is possible. Thanks to Joachim Breitner for spotting.
2012-09-10	LiftGet: vec-length is also known as subst (Vec A)	Helmut Grohne
	Thanks to Andres Löh for spotting.
2012-09-04	formulate List <-> Vec isomorphism problems	Helmut Grohne
	There are now like four open holes in LiftGet.agda that all boil down to the same problem. For proving equalities on Vec we first need to show that those Vecs actually have the same type. Proofs on two different levels are needed and somehow need to be merged.
2012-08-30	prove LiftGet.get-trafo-2-getlen	Helmut Grohne

2012-08-30	phrase other half of bijection in LiftGet	Helmut Grohne

2012-08-30	prove half of the bijection in LiftGet	Helmut Grohne

2012-08-30	give the type of different gets a name	Helmut Grohne

2012-08-06	attempt isomorphism between get on List and on Vec	Helmut Grohne
	Thus far we have found maps in both directions but lack statements about the composition of them.