[Agda] Automatic conversion between records and iterated Sigma types

[Martin Escardo]

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