[Agda] Setoid for List

[Serge D. Mechveliani]

On Wed, Jan 09, 2013 at 10:19:33AM +0100, Joachim Breitner wrote:
> Hello,
> 
> Am Dienstag, den 08.01.2013, 20:35 +0400 schrieb Serge D. Mechveliani:
> > If it does not, then is the following a reasonable program for this?
> > 
> >   listSetoid : {c l : Level} -> DecSetoid c l -> Setoid _ _
> >   listSetoid A = record{ Carrier       = List ACarr 
> >                        ; _\~~_         = eqList               
> >                        ; isEquivalence = isEquiv } 
> >       where    
> >       ACarr = DecSetoid.Carrier A                                   
> >       open DecSetoid {{...}}                                         
> >       eqList : Rel (List ACarr) _                                       
> >       eqList []        []        = \top                          
> >       eqList []        (_ :: _)  = \bot                                   
> >       eqList (_ :: _)  []        = \bot                                 
> >       eqList (x :: xs) (y :: ys)  with x \?= y                            
> >       ...                       | yes _ = eqList xs ys                    
> >       ...                       | _     = \bot
> >                                                                               
> >       isEquiv : IsEquivalence eqList            
> >       isEquiv =  <a proof, which I would have to set if not find in 
> >                   libraries>
> 
> I don't think you need DecSetoid to define Setoid for Lists. Here is my
> solution requiring only Setoid on the element types:
> 
> listSetoid : {c l : Level} -> Setoid c l -> Setoid _ _
> listSetoid {c} {l} A =
> [..]

>     open Setoid A
>     eqList : Rel (List ACarr) l                                    
>     eqList []        []       = Lift \top
> [..]
>     eqList (x :: xs) (y :: ys)  = x \~~ y \times eqList xs ys
>   

(I have substituted some math symbols).

I know this. But I doubt about efficiency for long lists.

 
> I also tried to give isEquiv, and it seems it worked, but agda still
> highlights eqRefl, eqSym and eqTrans in the last line as yellow, and I
> do not know why:
> [..]

I fear I would need to set some similar code.
But it is desirable to have such in the Standard Library for Agda.
Say,  Setoid, DecSetoid, TotalOrder ...  for  Product, List, Vector
-- these instances are very generic and fundamental.
My main question was: which of them are in the libraries?

Regards,

------
Sergei