[Agda] Automatic conversion between records and iterated Sigma types

[Martin Escardo]

On 13/04/2020 21:25, Thorsten Altenkirch wrote:
> I agree you want to do the meta theory using Sigma types but why do you need this during your development. I could also imagine a Agda backend that translate into some combinatory core language but I don’t think we need this within Agda.

Look at the proofs and constructions here, for example: 
https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#sip 
, sections 33-()1-(20)

They rely on properties of / and construction with Sigma (lots of them) 
for a uniform treatment.

This is mathematics and not meta-theory of the language used to develop 
the mathematics.

Martin