[Agda] Automatic conversion between records and iterated Sigma types

[Jesper Cockx]

Hi all,

I wrote a quick proof-of-concept of a macro to automatically translate a
record type to an iterated sigma type. There is a test case at the bottom
of
https://github.com/jespercockx/telescopic/blob/master/src/Telescopic/Record.agda,
which converts the sigma type into its encoding `Σ ℕ (λ x → Σ (Vec Bool x)
(λ x₁ → ·))`. (Note that while the file relies on my small library for
telescopes, the final result is just a vanilla iterated sigma type). If
there's interest, I might clean this up a bit and extend it to also
generate the functions back and forth and proofs that they are inverses.

-- Jesper

On Wed, Apr 15, 2020 at 12:48 AM Roman <effectfully at gmail.com> wrote:

> Sorry, I've been doing too much System F lately. I mean a dependent
> version of _×_ by "product" (i.e. Σ), not Π.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200415/1ec5cd25/attachment.html>