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

[Andrea Vezzosi]

The right to left direction of that equality seems inconsistent with MLTT.

Take

A = C = Bool
a = c = true

B true = Unit
B false = Unit

D true = Unit
D false = Bool

then you can prove ((A , a ≡ C , c) × (B a , b ≡ D c , d)) so you get
in particular Σ A B ≡ Σ C D.

But  Σ A B  has 2 elements, while  Σ C D  has 3 elements, so you can
disprove that equality.

Best,
Andrea

On Tue, Oct 6, 2015 at 12:38 PM, Matteo Acerbi <matteo.acerbi at gmail.com> wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda