<div dir="ltr"><div class="gmail_extra">On Tue, Oct 6, 2015 at 5:06 PM, Andrea Vezzosi <span dir="ltr"><<a href="mailto:sanzhiyan@gmail.com" target="_blank">sanzhiyan@gmail.com</a>></span> wrote:<br><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Assuming K, you should be able to implement P by using heterogeneous<br>
equality for _≅_.<br></blockquote><div><br><div class="gmail_default" style="font-family:monospace,monospace;display:inline">Did you mean the following?<br><br>data _≅_ {A : Set}(x : A) : {B : Set}(y : B) → Set where<br> refl : x ≅ x<br><br></div><div class="gmail_default" style="font-family:monospace,monospace">This is logically equivalent to equality of pointed types<br>(as in the HoTT blog post by Jesse McKeown).<br><br>to : {A : Set}{a : A}{B : Set}{b : B} → Eq (Σ Set id) (A , a) (B , b) → a ≅ b<br>to refl = refl<br>from : {A : Set}{a : A}{B : Set}{b : B} → a ≅ b → Eq (Σ Set id) (A , a) (B , b)<br>from refl = refl
<br><br></div><div class="gmail_default" style="font-family:monospace,monospace">Under UIP this is enough to conclude that they're isomorphic,<br>and your counterexample should be easy to recover.<br></div><div class="gmail_default" style="font-family:monospace,monospace"><br></div><div class="gmail_default" style="font-family:monospace,monospace">In my last email I used a postulated _≅_ in order to avoid<br></div><div class="gmail_default" style="font-family:monospace,monospace">that problem: but is that safe?<br></div></div></div></div></div>