[Agda] question about a form of irrelevance elimination

[Andrew Pitts]

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