[Agda] ≡ → ≈

[Twan van Laarhoven]

On 17/10/13 11:14, 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
>
> ...
>
> 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?

A _ in a pattern is like an unnamed variable. Using `PE.refl` is a case 
analysis, which is different from a variable match. Agda does not automatically 
translate _ into a case analysis, even for types with just one constructor.

> Is  ≡⇒≈  in Standard library?

It can't be, since you just defined ≈ yourself. If you postulate/define
   isEquivalence : IsEquivalence _≈_
then you do get
   IsEquivalence.reflexive isEquivalence : {x y : A} → x ≡ y → x ≈ y


Twan