# [Agda] Setoid for List

Serge D. Mechveliani mechvel at botik.ru
Wed Jan 9 11:28:12 CET 2013

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


More information about the Agda mailing list