[Agda] Prop in Agda 2.6

[Jon Sterling]

Hi Nicolai, thank you for this very insightful message!

Best,
Jon


On Wed, May 22, 2019, at 6:04 PM, Nicolai Kraus wrote:
> Hi Andy and Jon,
> 
> On Wed, May 22, 2019 at 10:04 PM Jon Sterling <jon at jonmsterling.com> wrote:
> > 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
> 
> just a small remark: the above "restricted equality reflection" already 
> implies full equality reflection, i.e. for m,n: A and p : Id(m,n), one 
> gets m=n (definitionally). This is because one can always consider the 
> type Σ(x: A).Id(m,x), for which the rules gives (m,refl) = (n,p), and 
> thus m = n.
> (It has been discussed before that, because of this, equality 
> reflection for contractible types is inconsistent in HoTT.) 
> Nicolai
>