[Agda] extending setoid

[Sergei Meshveliani]

On Mon, 2013-08-05 at 12:08 +0200, Andreas Abel wrote:
> Hi Sergei,
> 
> you could write a setoid transformer
> 
>    maybeSetoid : Setoid -> Setoid
>    maybeSetoid S =
>      record { Carrier = Maybe S.Carrier
>             ; ...
> 
> and then instantiate it with
> 
>    cardSetoid = maybeSetoid natSetoid
>    fooSetoid  = maybeSetoid foo1Setoid
> 
> etc.

Indeed, I see now. Thank you.

And I find  Data.Maybe.setoid  (call it Mb.setoid)  in Standard library
(with a nice and un-usual for me code, with ``data Eq'').

But to write `nothing' instead of `infinity' is not nice.
Therefore I add mapping a setoid from A by a map  f : Y -> Carrier A
:
 
mapSetoid : {c l l' : Level} → (A : Setoid c l) → (Y : Set l') →
                                    (Y → Setoid.Carrier A) → Setoid l' l
mapSetoid {c} {l} {l'} A Y f =  ...

data Cardinality : Set where  fin      : ℕ → Cardinality
                              infinity : Cardinality

natDecSetoid = DecTotalOrder.Eq.decSetoid natDTO   -- for ℕ 
natSetoid    = DecSetoid.setoid natDecSetoid

cardSetoid : Setoid _ _
cardSetoid = mapSetoid (Mb.setoid natSetoid) Cardinality f
             where
             f : Cardinality → Maybe ℕ
             f (fin n)  = just n
             f infinity = nothing

So, for a new extension  data Foo X,  X = Carrier A,
one need to 
1) define renaming  f : Foo X -> Maybe X,
2) apply  mapSetoid (Mb.setoid A) (Foo X) f.

Thanks,

------
Sergei


> 
> On 01.08.13 8:20 PM, Sergei Meshveliani wrote:
> > People,
> >
> > I wonder: how to generalize a default Setoid extension with a new value?
> >
> > For example, I write
> >
> > ---------------------------------------------------------------------
> > data Cardinality : Set where  fin      : ℕ → Cardinality
> >                                infinity : Cardinality
> >
> > -- That is   ℕ  U  infinity,
> > -- the equality extends in a standard way:
> >
> > cardSetoid : Setoid 0L 0L
> > cardSetoid = record{ Carrier       = Cardinality
> >                     ; _≈_           = _=c_
> >                     ; isEquivalence = isEquiv-c }
> >      where
> >      _=c_ : Rel Cardinality _
> >      (fin m)  =c (fin n)  =  m ≡ n
> >      infinity =c infinity =  ⊤
> >      _        =c _        =  ⊥
> >
> >      open IsEquivalence natEquiv using ()
> >                            renaming (sym to nSym; trans to nTrans)
> >      cRefl : Reflexive _=c_
> >      cRefl {fin m}    = refl
> >      cRefl {infinity} = ⊤.tt
> >
> >      cTrans : Transitive _=c_
> >      cTrans {infinity} {_}      {infinity} _    _    =  cRefl
> >      cTrans {fin k}    {fin .k} {fin .k}   refl refl =  refl
> >
> >      cTrans {_}        {fin _}    {infinity} _    y='z =  ⊥-elim y='z
> >      cTrans {_}        {infinity} {fin _}    _    y='z =  ⊥-elim y='z
> >      cTrans {fin _}    {infinity} {_}        x='y _    =  ⊥-elim x='y
> >      cTrans {infinity} {fin _}    {_}        x='y _    =  ⊥-elim x='y
> >
> >      cSym : ...
> >      ...
> >
> >      isEquiv-c = record{ refl = cRefl; sym = cSym; trans = cTrans }
> > --------------------------------------------------------------------
> >
> > Next time it may be, say,
> >
> >    data Foo : Set where foo1 : Foo1 → Foo
> >                         foo2 : Foo,
> >
> > and a similar code will need to repeat.
> > [..]