[Agda] Heterogeneous equality of pairs and records: some questions.

[Matteo Acerbi]

Hello,

a recent thread started by Martín Escardó on the Homotopy Type Theory
list prompted me to dig up some old code of mine, on which I would
appreciate some feedback from you.

I cleaned up the definitions, added some comments and questions, and
pushed it here:

https://gist.github.com/ma82/0b747c314cb1acc5efaa

The questions are at the end of the file.

The main one is:

  Can we assume

  (Σ A B , a , b ≡ Σ C D , c , d) ≡ ((A , a ≡ C , c) × (B a , b ≡ D c , d))

  ?

There are several others, though, together with some observations of mine.

Since it is an Agda file, I am asking for feedback here: however, I
would appreciate any comment, even if not precisely Agda-related, or
even if not answering any of those questions at all.

Thanks in advance to anyone who will comment!

Cheers,
Matteo