<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 "irrelevance in execution", also sometimes called "erasability", is a stronger principle that invokes meta-level properties that are not internalized, in particular canonicity/adequacy (formal results on the normal forms of "closed" 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 "Inductive Families Need Not Store Their Indices" (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, "Run-Time Optimisation").<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"><<a href="mailto:monnier@iro.umontreal.ca" target="_blank">monnier@iro.umontreal.ca</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">> The literature is full of work which erroneously conflates irrelevance in<br>
> 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>