<div dir="ltr"><div>Hi Jacques,</div><div><br></div><div>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.</div><div><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, Apr 13, 2020 at 9:20 PM Jacques Carette <<a href="mailto:carette@mcmaster.ca">carette@mcmaster.ca</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Very hard, I believe.  Lines 1113 and 1114<br>
<br>
   let u := fresh "u" in<br>
   let v := fresh "v" in<br>
<br>
in particular.  See the comment by @jespercockx on <br>
<a href="https://github.com/agda/agda/issues/3699" rel="noreferrer" target="_blank">https://github.com/agda/agda/issues/3699</a>.<br>
<br>
Jacques<br>
<br>
On 2020-04-13 3:11 p.m., Bas Spitters wrote:<br>
> This is what the issig tactic does in the HoTT library. I don't know<br>
> how difficult it is to convert it to agda.<br>
> <a href="https://github.com/HoTT/HoTT/blob/master/theories/Basics/Overture.v" rel="noreferrer" target="_blank">https://github.com/HoTT/HoTT/blob/master/theories/Basics/Overture.v</a><br>
><br>
> On Mon, Apr 13, 2020 at 8:47 PM Martin Escardo <<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a>> wrote:<br>
>> Is it possible to write a tactic to convert between records and<br>
>> equivalent iterated Sigma types? And, if so, to also produce code to<br>
>> establish their equivalence?<br>
>><br>
>> Thanks,<br>
>> Martin<br>
>> _______________________________________________<br>
>> Agda mailing list<br>
>> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
>> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>