[Agda] with x=?x

[Wolfram Kahl]

On Wed, Dec 31, 2014 at 10:16:36PM +0400, Sergei Meshveliani wrote:
> I have  x : K,  _≈_ and _≟_  on K  (of a DecSetoid over Carrier = K).
> And try you suggestion: 
> 
>   x≟x≡yes : (x : K) → (x ≟ x) ≡ (yes ≈refl)
>   x≟x≡yes x  with x ≟ x
>   ...             | yes x≈x =  ...PropositionalEquality.refl
>   ...             | no x≉x  =  ⊥-elim $ x≉x ≈refl
> 
> This is not type-checked. 
> I do not know, something needs to be fixed here ... 

No: Consider the case where K is \top,
with one element tt, and (tt ≈ tt) is defined to be Bool,
(or anything else containing at least two elements).
Then complete the DecSetoid instance such that:

(tt ≟ tt) = yes false
≈refl {x = tt} = true

Then  x≟x≡yes does not hold.


Wolfram