Nils Anders Danielsson

> I do not think it is useful to build the coding styles of the current libraries into the language itself. We could go with your approach, but in that...

I think one should also ensure that no variable is used twice in the solution.

> What if the 'proper' long normal form was `λ {record {l = l; r = r} → c l r}` instead ? Then everything is much more clearly linear....

> I'm using pattern-matching lambda, as in > > ```agda > postulate D : Set > record XX : Set where > constructor c > field > l : D...

I prefer bag/set equivalence to bag/set equality. (I used to refer to the relations as equalities, but Fritz Henglein convinced me that the term equivalence is better.)