[Agda] Automatic conversion between records and iterated Sigma types

[Anders Mortberg]

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