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

[Matteo Acerbi]

On Tue, Oct 6, 2015 at 5:06 PM, Andrea Vezzosi <sanzhiyan at gmail.com> wrote:

> Assuming K, you should be able to implement P by using heterogeneous
> equality for _≅_.
>

Did you mean the following?

data _≅_ {A : Set}(x : A) : {B : Set}(y : B) → Set where
  refl : x ≅ x

This is logically equivalent to equality of pointed types
(as in the HoTT blog post by Jesse McKeown).

to : {A : Set}{a : A}{B : Set}{b : B} → Eq (Σ Set id) (A , a) (B , b) → a ≅
b
to refl = refl
from : {A : Set}{a : A}{B : Set}{b : B} → a ≅ b → Eq (Σ Set id) (A , a) (B
, b)
from refl = refl

Under UIP this is enough to conclude that they're isomorphic,
and your counterexample should be easy to recover.

In my last email I used a postulated _≅_ in order to avoid
that problem: but is that safe?​
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151006/9dc02a9b/attachment.html