<div dir="ltr"><div>Hi all,</div><div><br></div><div>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 <a href="https://github.com/jespercockx/telescopic/blob/master/src/Telescopic/Record.agda">https://github.com/jespercockx/telescopic/blob/master/src/Telescopic/Record.agda</a>, 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.</div><div><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Apr 15, 2020 at 12:48 AM Roman <<a href="mailto:effectfully@gmail.com">effectfully@gmail.com</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">Sorry, I've been doing too much System F lately. I mean a dependent<br>
version of _×_ by "product" (i.e. Σ), not Π.<br>
</blockquote></div>