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

[Andrea Vezzosi]

Oh, you are right, I was going by analogy to how het. equality can be
used when stating congruence of constructors of record types, but in
those cases we already know that C = D by construction.

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?


On Tue, Oct 6, 2015 at 6:27 PM, Matteo Acerbi <matteo.acerbi at gmail.com> wrote:
> 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?