[Agda] question about a form of irrelevance elimination

[Thorsten Altenkirch]

Hi Neel & Andy,

I too think that Andy’s proposal is problematic at least if we add the
definitional equality to the eliminator

!-elim p [ a ] == a

Because this would destroy decidability and termination in an inconsistent
context. That is if we assume that all types are equal we can type check
and reduce untyped programs.

I don’t understand your argument, because surely we should be allowed to
ignore values in closed propositions.

Btw, I do think that Andy’s rule even with the equation above is logically
sound and that it isn’t such a problem if you have divergent programs
after you have assumed that pigs can fly.

Thorsten

On 14/07/2015 10:07, "Neelakantan Krishnaswami"
<n.krishnaswami at cs.bham.ac.uk> wrote:

>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.Irrelevan
>>ce).
>> 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
>>
>_______________________________________________
>Agda mailing list
>Agda at lists.chalmers.se
>https://lists.chalmers.se/mailman/listinfo/agda





This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please send it back to me, and immediately delete it. 

Please do not use, copy or disclose the information contained in this
message or in any attachment.  Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.

This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.