<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><br><div><div>On 16 Feb 2011, at 11:48, Andreas Abel wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div>Hi Thorsten,<br><br>On 2/16/11 1:17 PM, Thorsten Altenkirch wrote:<br><blockquote type="cite">Btw, I completely agree with Peter Hancock that we should use/look<br></blockquote><blockquote type="cite">for a computational sound interpretation of ext (such as OTT).<br></blockquote><blockquote type="cite">However, OTT and my earlier LICS paper rely on proof irrelevance<br></blockquote><blockquote type="cite">which is incompatible with the recent developments related to<br></blockquote><blockquote type="cite">univalent foundations (which is basically a strengthening of ext by<br></blockquote><blockquote type="cite">considering an extensional equality of sets called weak<br></blockquote><blockquote type="cite">equivalence).<br></blockquote><br>Proofs of small equalities (equalities between terms) can still be irrelevant, as I understood it. It is sufficient to have one proof of 0=0, since there are no isomorphisms between 0 and 0. ;-)<br></div></blockquote><div><br></div><div>Yes, all small sets (i.e. A : Set_0) have H-level 2, i.e. UIP holds. However, this is rather a coincidence which may fail to hold in the future - in particular if one introduces proof-relevant quotients.</div><div><br></div><blockquote type="cite"><div>Can't OTT work with that restricted proof irrelevance?<font class="Apple-style-span" color="#000000"><font class="Apple-style-span" color="#144FAE"><br></font></font></div></blockquote><div><br></div><div>If you restrict yourself to Set_0. But this seems quite unnatural.</div><div><br></div><div>Cheers,</div><div>Thorsten</div></div><br></body></html>