[Agda] Automatic conversion between records and iterated Sigma types

[Jesper Cockx]

Hi Jacques,

Note that it *is* possible to generate fresh names from Agda's reflection
machinery, it is just not possible to access those generated names from
outside of the macro call. But if you're willing to give just one name
manually to the top-level definition (e.g. a value of a record type
containing fields for the iterated sigma type itself, functions converting
back and forth, and proofs about them) then the current reflection
machinery should work just fine. In particular, there should be no need to
generate new datatypes, which is the main bottleneck in #3699.

-- Jesper

On Mon, Apr 13, 2020 at 9:20 PM Jacques Carette <carette at mcmaster.ca> wrote:

> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200414/d24c1f57/attachment.html>