[Agda] standard instance proposal

[Serge D. Mechveliani]

On Thu, Jan 10, 2013 at 07:09:16PM +0400, Serge D. Mechveliani wrote:
> [..]
> Here is a certain  Product & List instance  proposal for 
> Standard Library.
> (I)
>   productSetoid : {c l c' l' : Level} -> (A : Setoid c  l ) -> 
>                                          (B : Setoid c' l') -> Setoid _ _
> 
> builds the setoid  A x B  for setoids A and B  defined by the standard
> law for direct product
> [..]
> (II) listSetoid  for  List   needs to be defined similarly 
> [..]

Probably, Standard lib-0.6  already has  (I) and (II)  
(for Setoid and DecSetoid).
As people write,    Relation.Binary.Product.Pointwise  implements  (I),
and now I see that, probably,
                    Relation.Binary.List.Pointwise     implements  (II).

It remains

> (III)
>   setoidByMap : {c c' l' : Level} -> (C : Set c) -> (B : Setoid c' l') ->
>                                      (C -> Setoid.Carrier B) -> Setoid _ _
> 
> builds the setoid  A  on  C  from a setoid  B  and a map 
> f : C -> Carrier B   -- in a natural way:
> a =C a' =  f a \~~ f a'.    
> 
> (is such in the library?).

Regards,

------
Sergei