[Agda] Automatic conversion between records and iterated Sigma types

[Martin Escardo]

Musa has kindly produced such a mechanism using emacs lisp, and allowed 
me to advertise it here:

On 14/04/2020 06:28, alhassy at gmail.com wrote:> Good morning Martin,
 >
 > I've written a little Emacs editor tactic in the style of Agda's
 > ``auto'' mechanism.
 >
 > https://gist.github.com/alhassy/a4ce4032e7c33de874c3ce43dc9b0fe1
 >
 > 0. Select, highlight, the record you are interested in;
 > 1. Press C-x C-t to have a Sigma type and coercion to be created;
 > 2. Paste in the Sigma type, and coercion, with C-y wherever you like.
 >
 > The example usage shows that this editor tactic can handle (seemingly)
 > arbitrary definitions interleaved among field declarations.
 >
 > Hope this helps,
 >
 > Musa

On 14/04/2020 08:55, andersmortberg at gmail.com wrote:
> We would love to have this tactic in the agda/cubical library as well
> for the same reason as Martin. See e.g.
> https://github.com/agda/cubical/issues/279
> 
> --
> Anders
> 
> On Mon, Apr 13, 2020 at 10:31 PM Martin Escardo <m.escardo at cs.bham.ac.uk> wrote:
>>
>>
>>
>> On 13/04/2020 21:25, Thorsten Altenkirch wrote:
>>> I agree you want to do the meta theory using Sigma types but why do you need this during your development. I could also imagine a Agda backend that translate into some combinatory core language but I don’t think we need this within Agda.
>>
>> Look at the proofs and constructions here, for example:
>> https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#sip
>> , sections 33-()1-(20)
>>
>> They rely on properties of / and construction with Sigma (lots of them)
>> for a uniform treatment.
>>
>> This is mathematics and not meta-theory of the language used to develop
>> the mathematics.
>>
>> Martin
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe