[Agda] extending setoid

Sergei Meshveliani mechvel at botik.ru
Thu Aug 1 20:20:40 CEST 2013

```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

```