[Agda] question about a form of irrelevance elimination

[Dan Doel]

On Tue, Jul 14, 2015 at 9:34 AM, Neelakantan Krishnaswami
<n.krishnaswami at cs.bham.ac.uk> wrote:
>
> That said, I think HoTT-style truncation (where elements are
> propositionally equal, but we don't put it in the definitional
> equality) is incompatible with computational erasure, because the
> eliminator for it lets you use a truncated value to compute an element
> of a truncated singleton type, and then un-truncate it. So it
> seems to me that you have to pass it around.

This seems likely to me. Computational irrelevance as far as erasability
goes turns out to be subtly different from being propositional. The thesis
on it by Richard Nathan Mishra-Linger* goes into some negative consequences
of even things Agda allows, like eliminating irrelevant empty types. I think
Agda's irrelevance is still intended to be similar to this sort of irrelevance.

Martin Escardo wrote:
>
> "No more erasing ..."

This doesn't say that Agda's irrelevance annotations have fundamentally
changed in scope to no longer be about erasable/parametric arguments. It
just says (I think) that Agda no longer erases them and replaces them with
'_' during symbolic evaluation and such.

[*] http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.154.5619