[Agda] question about a form of irrelevance elimination

[Martin Escardo]

On 14/07/15 10:07, Neelakantan Krishnaswami 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.

See


http://wiki.portal.chalmers.se/agda/agda.php?n=ReferenceManual.Irrelevance#Nomoreerasing

 "No more erasing

  Irrelevant things are no longer erased internally. This means that
  they are printed as ordinary terms, not as “_” as before.
 "

Nevertheless, I think you still don't get propositional truncations with
irrelevant fields.

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

I am a bit nervous about the computational consistency of this
postulate. I think this may imply excluded middle (but I am not sure).

Martin


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

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe