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

[Matteo Acerbi]

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. :-)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151006/6c90e7f0/attachment.html