[Agda] Automatic conversion between records and iterated Sigma types

[Jacques Carette]

Thanks Jesper.

I don't think I fully follow though.  Is it possible to use reflection 
to take in a (nested) Sigma type (say the one for Monoid) and return the 
declaration of the associated record type? Could I take the name of the 
bound variables in that Sigma type as the labels of the resulting record 
type?  That would be perfect. I did not think that was possible. I would 
love to be wrong here!

Jacques

On 2020-04-14 4:07 a.m., Jesper Cockx wrote:
> 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 
> <mailto: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 <mailto: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 <mailto:Agda at lists.chalmers.se>
>     >> https://lists.chalmers.se/mailman/listinfo/agda
>     > _______________________________________________
>     > Agda mailing list
>     > Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     > https://lists.chalmers.se/mailman/listinfo/agda
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto: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/f2911170/attachment.html>