[Agda] question about a form of irrelevance elimination

[Martin Escardo]

Andy, we wondered when we get [A]->A where [-] is your !, without any
postulates.

There are a number of situations where this holds:
http://www.cs.bham.ac.uk/~mhe/Bracket/Bracket.html

(In the file, "irrelevant A" is defined to be [A]->A. The file
investigates which types are irrelevant in this sense.)

But I don't think this can be used as a propositional truncation as in
the HoTT book, because all elements of [A] are definitionally equal.

You always have [A] -> ¬¬A, as a consequence that [0]->0.

I don't think you can prove ¬¬A -> [A].

But also I don't think you can distinguish [A] from ¬¬A.

Martin

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
> 

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