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

[Andrea Vezzosi]

Considering the other thread, maybe you could think of _≅_ as just
"material" equality, i.e. comparing the elements on the nose with no
regard for which sets/types they are a member of.

That would mean that propositional equality also needs to be
interpreted that way otherwise ≡→≅ would be unsound.
That's not unusual for a set-theoretic model of MLTT+K though, I believe.


On Tue, Oct 6, 2015 at 7:02 PM, Matteo Acerbi <matteo.acerbi at gmail.com> wrote:
> On Tue, Oct 6, 2015 at 6:50 PM, Andrea Vezzosi <sanzhiyan at gmail.com> wrote:
>>
>> I don't know if the existence of a _≅_ as described by P is a
>> consistent assumption then, do you have some model in mind?
>
>
> What happens in the set-theoretic model of Agda --with-K?
>
> Unfortunately I am not very competent on models of Type Theory,
> though I'd like to know more, sooner or later. :-)