[Agda] Automatic conversion between records and iterated Sigma types

[Bas Spitters]

The tactic is used in precisely the way Martin describes in the HoTT
library in Coq. It's a very convenient tactic.

On Mon, Apr 13, 2020 at 9:34 PM Martin Escardo <m.escardo at cs.bham.ac.uk> wrote:
>
> Because records are more convenient notationally, but Sigma types are
> more convenient mathematically, as they allow a uniform treatment. You
> can prove loads of preservation properties for Sigma formation, and if
> you use records you have to repeat these proofs. A record *is* the same
> thing as an iterated Sigma type, and this needs to be made official from
> a mathematical point of view. This is particularly important in
> univalent mathematics. The only reason I don't use record types in my
> developments is this. I would rather use records, but then I would need
> to reprove everything again, or transport it along equivalences (and
> none of these two options is attractive). Martin
>
> On 13/04/2020 20:25, Thorsten Altenkirch wrote:
> > Why would anybody do something like this?
> >
> > Sent from my iPhone
> >
> >> On 13 Apr 2020, at 19:48, 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
> >
> >
> >
> > This message and any attachment are intended solely for the addressee
> > and may contain confidential information. If you have received this
> > message in error, please contact the sender and delete the email and
> > attachment.
> >
> > Any views or opinions expressed by the author of this email do not
> > necessarily reflect the views of the University of Nottingham. Email
> > communications with the University of Nottingham may be monitored
> > where permitted by law.
> >
> >
> >
> >
>
> --
> Martin Escardo
> http://www.cs.bham.ac.uk/~mhe
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda