[Agda] Automatic conversion between records and iterated Sigma types

[Roman]

Jesper,

> Indeed, automatically converting from an iterated sigma type into a record type would require generating fresh top-level names for the fields of the record, which is currently not possible.

but as you said one could just ask the user to provide the top-level
names manually. Which is something I would expect from such a
machinery anyway.

Martin, why not just define some kind of product type with a `String`
name associated with its first projection? Such iterated products
would give you what is essentially records while still having nice
metatheoretical properties.

In general implementing `record -> iterated Sigma` + their isomorphism
using reflection is certainly feasible in Agda, I have a library that
handles general inductive types [1], but it doesn't handle the
particular corner case of iterated non-inductive products well (no eta
rules), although it's not a theoretical limitation, just a deficiency
in the implementation.

[1] https://github.com/effectfully/Generic