[Agda] Automatic conversion between records and iterated Sigma types

[Martin Escardo]

Is it possible to write a tactic to convert between records and 
equivalent iterated Sigma types? And, if so, to also produce code to 
establish their equivalence?

Thanks,
Martin