<div dir="ltr"><div dir="ltr"><div>Hi Andy and Jon,</div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, May 22, 2019 at 10:04 PM Jon Sterling <<a href="mailto:jon@jonmsterling.com">jon@jonmsterling.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Indeed, I note that if you have such a REWRITE rule, then you can prove the following instance of equality reflection:<br>
<br>
     M, N : A              P : is-prop(A)<br>
 -----------------------------------------<br>
    M = N : A<br></blockquote><div><br></div><div>just a small remark: the above "restricted equality reflection" already implies full equality reflection, i.e. for m,n: A and p : Id(m,n), one gets m=n (definitionally). This is because one can always consider the type Σ(x: A).Id(m,x), for which the rules gives (m,refl) = (n,p), and thus m = n.</div><div>(It has been discussed before that, because of this, equality reflection for contractible types is inconsistent in HoTT.) </div><div>Nicolai</div><div><br></div></div></div></div>