<div dir="ltr"><div>I would say that irrelevance in type-checking is *internalized* irrelevance having a first-class status in the language (in particular in open terms). What Conor calls &quot;irrelevance in execution&quot;, also sometimes called &quot;erasability&quot;, is a stronger principle that invokes meta-level properties that are not internalized, in particular canonicity/adequacy (formal results on the normal forms of &quot;closed&quot; inhabitants of a given type). The key may be the empty context (but I think we can extend this to an interesting richer class of context), but the door it opens is made of canonicity/adequacy results. In particular, such results can be broken by introducing axioms (are axioms counted as part of the context?) -- whether they are preserved by univalence is the hot question.<br><br></div>On this distinction I like &quot;Inductive Families Need Not Store Their Indices&quot; (Edwin Brady, Conor McBride, James McKinna, 2003), which presents and contrasts many different shades of erasability (the distinction on the empty context is discussed in Section 5, &quot;Run-Time Optimisation&quot;).<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Feb 24, 2015 at 11:15 PM, Stefan Monnier <span dir="ltr">&lt;<a href="mailto:monnier@iro.umontreal.ca" target="_blank">monnier@iro.umontreal.ca</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">&gt; The literature is full of work which erroneously conflates irrelevance in<br>
&gt; typechecking with irrelevance in execution.<br>
<br>
</span>IIUC, the key reason for the difference is that evaluation always<br>
proceeds in the empty context, right?<br>
<span class="HOEnZb"><font color="#888888"><br>
<br>
        Stefan<br>
</font></span><div class="HOEnZb"><div class="h5"><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>