[Agda] Re: Fin n -> Fin n extensional?

[Gabriel Scherer]

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.

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").

On Tue, Feb 24, 2015 at 11:15 PM, Stefan Monnier <monnier at iro.umontreal.ca>
wrote:

> > The literature is full of work which erroneously conflates irrelevance in
> > typechecking with irrelevance in execution.
>
> IIUC, the key reason for the difference is that evaluation always
> proceeds in the empty context, right?
>
>
>         Stefan
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150225/ccf920f9/attachment.html