[Agda] Automatic conversion between records and iterated Sigma types

[Jacques Carette]

Very hard, I believe.  Lines 1113 and 1114

   let u := fresh "u" in
   let v := fresh "v" in

in particular.  See the comment by @jespercockx on 
https://github.com/agda/agda/issues/3699.

Jacques

On 2020-04-13 3:11 p.m., Bas Spitters wrote:
> This is what the issig tactic does in the HoTT library. I don't know
> how difficult it is to convert it to agda.
> https://github.com/HoTT/HoTT/blob/master/theories/Basics/Overture.v
>
> On Mon, Apr 13, 2020 at 8:47 PM Martin Escardo <m.escardo at cs.bham.ac.uk> wrote:
>> 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
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda