[Agda] Prop in Agda 2.6

[Nicolai Kraus]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190523/91148108/attachment.html>