[Agda] without-K problem

[Guillaume Brunerie]

Hi all,

For what it’s worth, I cannot reproduce the bug using the following
definition of the identity types:

data _≡_ {A : Set} : A → A → Set where
  refl : {x : A} → x ≡ x

But I can reproduce it using the following definition (which is the one
used in the standard library):

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x


Guillaume

2012/6/18 Altenkirch Thorsten <psztxa at exmail.nottingham.ac.uk>

> Hi Nisse,
>
> I noticed that a weak version of K is provable even though the without-K
> flag is set:
>
> {-# OPTIONS --without-K #-}
> module K-bug where
>
> open import Relation.Binary.PropositionalEquality
>
> weakK : {A : Set}{a b : A}(p q : a ≡ b)(α β : p ≡ q) → α ≡ β
> weakK refl .refl refl refl = refl
>
> This would imply that all types have dimension of at most 3. I don't think
> it is provable with J.
>
> A simpler term which is provable but shouldn't was found by my student
> Nicolai:
>
> weak2 : {A : Set} {a : A} (α : refl {x = a} ≡ refl) → α ≡ refl
> weak2 refl = refl
>
> It seems to me that these patterns satisfy the specification of without-K
> (I.e. the condition is too weak).
>
> Do you see a fix?
>
> Cheers,
> Thorsten
>
>  This message and any attachment are intended solely for the addressee and
> may contain confidential information. If you have received this message in
> error, please send it back to me, and immediately delete it. Please do not
> use, copy or disclose the information contained in this message or in any
> attachment. Any views or opinions expressed by the author of this email do
> not necessarily reflect the views of the University of Nottingham.
>
> This message has been checked for viruses but the contents of an
> attachment may still contain software viruses which could damage your
> computer system: you are advised to perform your own checks. Email
> communications with the University of Nottingham may be monitored as
> permitted by UK legislation.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120618/c63de233/attachment.html