[Agda] Prop in Agda 2.6

[Jon Sterling]

Hi Andy,

This seems consistent with an interpretation of non-cubical agda into extensional type theory, but I just want to mention something I'd noticed before: if you wanted to add 'untrunc' to Agda, you might be tempted to have a beta rule. But this appropriate beta rule would induce equality reflection for proofs of propositions, which one probably doesn't want in the formal system.

Best,
Jon



On Wed, May 22, 2019, at 12:47 PM, Andrew Pitts wrote:
> 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
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>