[Agda] ≡ → ≈

[Sergei Meshveliani]

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?

Is  ≡⇒≈  in Standard library?

Thanks,

------
Sergei