[Agda] Automatic conversion between records and iterated Sigma types

[Bas Spitters]

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