<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Feb 19, 2015 at 3:54 PM, Abhishek Anand <span dir="ltr">&lt;<a href="mailto:abhishek.anand.iitg@gmail.com" target="_blank" onclick="window.open(&#39;https://mail.google.com/mail/?view=cm&amp;tf=1&amp;to=abhishek.anand.iitg@gmail.com&amp;cc=&amp;bcc=&amp;su=&amp;body=&#39;,&#39;_blank&#39;);return false;">abhishek.anand.iitg@gmail.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">In other words, is it true that in Agda with K, any proof of equality (Id) of closed terms computes down to refl?</blockquote></div><br>I don&#39;t know what the conditions are for Agda&#39;s type theory to be strongly normalizing on Id types.  I suspect it still holds with K, but I haven&#39;t looked at any details.</div></div>