[Agda] ≡ → ≈

[Wolfram Kahl]

On Thu, Oct 17, 2013 at 02:14:18PM +0400, Sergei Meshveliani wrote:
> Please, what is the simplest program for  ≡ ⇒ ≈  ?
> 
>   open import Relation.Binary.PropositionalEquality as PE using (_≡_)
> 
>   postulate A     : Set
>   postulate _≈_   : Rel A 0ℓ  
>   postulate ≈refl : Reflexive _≈_
> 
>   ≡⇒≈ : {x y : A} → x ≡ y → x ≈ y
>   ≡⇒≈ PE.refl =  ≈refl
> 
> I have spent 20 minutes to find it. The attempts were
>  
> (1)  ≡⇒≈ _ = ≈refl  
> ,
> (2)  ≡⇒≈ e = e                 (type mismatch) 
> ,
> (3)  ≡⇒≈ {x} {.x} _ = ≈refl    ("cannot infer ... dotted pattern ...")
> ,
> (4)  ≡⇒≈ {x} {.x} PE.refl =  ≈refl      (works!)
> ,
> (5)  ≡⇒≈ PE.refl =  ≈refl               (also works!)
> 
> 
> The checker sees that  PE.refl  is the only value in  x ≡ y,
> so it needs to put  PE.refl  for `_'.
> Why does not it?

Because it sees no reason why |x| and |y| should be the same.

> Is  ≡⇒≈  in Standard library?

Under the name |reflexive| (at least in Setoid).


Wolfram