[Agda] extending setoid

[Sergei Meshveliani]

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.

If  Foo1  is of Setoid, then  _≈_  extends to  Foo  by default.
So, one can imagine a function

    deriveExtendedSetoid : ...

Has anybody organized such a generalization?
May be, Standard library has some support?

Regards,

------
Sergei