[Agda] Associativity for free!

[Alan Jeffrey]

On 11/04/2011 05:48 AM, Nils Anders Danielsson wrote:
> On 2011-10-26 16:48, Alan Jeffrey wrote:
>> The idea of using difference lists to represent lists is standard, but
>> as far as I know, this use of irrelevant equalities to get structural
>> recursion is new. Anyone know of any prior art?
>
> I've used the two tricks independently, but I haven't seen them used
> together.

This is my feeling, that the two tricks have been kicking around for a 
while, and this is just the requisite bit of glue to stick them together.

> However, in the end I decided not to use this approach, because I didn't
> want to rely on yet another not-universally-accepted feature of Agda.

Indeed. I'm on thin ice here, as the postulate for relevance of 
propositional equality is a bit dodgy. I'm not entirely sure how it 
would be formalized in homotopy types (it implies that there is a 
canonical path between any two connected points, but who knows what that 
does to the theory).

A.