[Agda] question about a form of irrelevance elimination

[Neelakantan Krishnaswami]

Dear Andy,

It looks like the escape property you describe is equivalent to the
universal property of truncation in HoTT. Adding it means that
irrelevance is basically the same as quotienting by the full relation.
(See Kraus et al's "Notions of Anonymous Existence in Martin-Loef Type
Theory".)

However, this has the effect that irrelevant arguments cannot be
erased at runtime; you still need to pass them around in case you
use an irrelevant argument to construct an escaping value.

So, it's consistent to add, but if you care about running dependently
typed programs (as opposed to typechecking them), you might not want to
add it. :)

Best,
Neel


On 14/07/15 09:48, Andrew Pitts wrote:
> Since version 2.2.8, Agda supports irrelevancy annotations
> (http://wiki.portal.chalmers.se/agda/agda.php?n=ReferenceManual.Irrelevance).
> Among other things this allows one to define a form of truncation:
>
> record ! {ℓ : Level}(A : Set ℓ) : Set ℓ where
>    constructor ![_]
>    field
>      .prf : A
> open ! public
>
> Since the elements of ! A are definitionally irrelevant, they are also
> propositionally irrelevant, i.e. ! A is a proposition in the sense of
> Homotopy Type Theory:
>
> isProp : {ℓ : Level}(A : Set ℓ) → Set ℓ
> isProp A = (x y : A) → x ≡ y
> !isprop : {ℓ : Level}{A : Set ℓ} → isProp (! A)
> !isprop _ _ = refl
>
> I would like to be able to escape from an irrelevant context in the
> case of propositions:
>
> postulate
>    !elim : {ℓ : Level}{A : Set ℓ}.(_ : isProp A) → (! A) → A
>
> Does adding such a postulate destroy logical consistency?
>
> Andy Pitts
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>