[Agda] extending setoid

[Andreas Abel]

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.

Best,
Andreas

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.
>
> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/