[Agda] Prop in Agda 2.6

[Jon Sterling]

Dear Andy,

On Wed, May 22, 2019, at 2:50 PM, Andrew Pitts wrote:
> Dear John,
> 
> > On 22 May 2019, at 18:28, Jon Sterling <jon at jonmsterling.com> wrote:
> > 
> > Hi Andy,
> > 
> > This seems consistent with an interpretation of non-cubical agda into extensional type theory,
> 
> or, to put it crudely, the set theoretic model of type theory can give 
> a model of these axioms.
> 
> > 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.
> 
> Interesting. Can we clarify what you mean? If A : Set and e : isProp A, 
> then for any x : A we have that untrunc e (squash x) and x are 
> propositionally equal (using e). Conversely for any y :  ∥ A ∥ we have 
> that squash (untrunc e y) and y are both elements of ∥ A ∥ in Prop and 
> so are definitionally equal. Were you suggesting not making a REWRITE 
> for untrunc e (squash x) and x? (I don’t think I need to)

Indeed, I note that if you have such a REWRITE rule, then you can prove the following instance of equality reflection:

     M, N : A              P : is-prop(A)
 -----------------------------------------
    M = N : A

The proof works as follows:

1. I have squash(M) == squash(N) : is-prop(A) by proof irrelevance
2. I have untrunc(P,squash(M)) == untrunc(P,squash(N)) : A by the congruence with untrunc
3. I have M == N : A by transitivity on both sides with the judgmental beta rule

This is why in the proof assistant, one would not want to construe the beta principle for unsquash as a judgmental rewrite.

Best,
Jon


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