[Agda] Prop in Agda 2.6

[Andrew Pitts]

I’m interested in using the built-in sort of definitionally proof-irrelevant propositions that Agda 2.6 introduced. I have readthedocs at <https://agda.readthedocs.io/en/latest/language/prop.html>.

For the development I have in mind (which assumes axiom K) I need Prop to be extensional

postulate
  propext :
    {l : Level}
    {P Q : Prop l}
    (_ : P → Q)
    (_ : Q → P)
    → ------------
    P ≡ Q

and to be able to “untruncate hprops" (in particular, to be able to untruncate identity types, in the presence of axiom K).

data ∥_∥ {l : Level}(A : Set l) : Prop l where
  squash : A → ∥ A ∥

isProp : {l : Level} → Set l → Set l
isProp A = (x y : A) → x ≡ y

postulate
  untrunc :
    {l : Level}
     {A : Set l}
     (_ : isProp A)
     → ------------
     ∥ A ∥ → A

Neither of the postulates propext or untrunc is provable in Agda 2.6, is it?

I think they are logically consistent axioms. But is there a better way than just postulating them?

Andy