[Agda] (All P) Respects =pointwise

[Nils Anders Danielsson]

On 2015-12-02 14:24, Sergei Meshveliani wrote:
> Has Standard library something for this:
>
>    cong-All-pointwise : ∀ {p} {P : C → Set p} → P Respects _≈_ →
>                                                 (All P) Respects _=l_
> ?

I don't think so.

-- 
/NAD