[Agda] Automatic conversion between records and iterated Sigma types

[Roman]

Sorry, I've been doing too much System F lately. I mean a dependent
version of _×_ by "product" (i.e. Σ), not Π.