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

Age	Commit message (Collapse)	Author
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.