[Agda] extending equality

[Matus Tejiscak]

Hello, you could shorten it as, for example,

   cSym : Symmetric _=c_
   cSym {infinity} {infinity} tt    = tt
   cSym {fin m}    {fin .m}   nRefl = nRefl
   cSym {infinity} {fin _}    ()
   cSym {fin _}    {infinity} ()

which does not omit the two impossible cases but is a bit simpler overall.

In this variant, you need to match on the nRefl (instead of putting an  
underscore there) in order to unify m and n in the typechecker.

Matus

Quoting Sergei Meshveliani <mechvel at botik.ru>:

> How do you think, please,
> is there possible a simpler expression for  cSym  below?
>
> -------------------------------------------------------------
> data Cardinality : Set where  fin      : ℕ → Cardinality
>                               infinity : Cardinality
> _=c_ : Rel Cardinality _
> (fin m)  =c (fin n)  =  m ≡ n
> infinity =c infinity =  ⊤
> _        =c _        =  ⊥
>
> natDecSetoid = DecTotalOrder.Eq.decSetoid natDTO    -- for ℕ
> natSetoid    = DecSetoid.setoid natDecSetoid
> natEquiv     = Setoid.isEquivalence natSetoid
>
> open IsEquivalence natEquiv renaming
>                           (refl to nRefl; sym to nSym; trans to nTrans)
> _≟_ = DecSetoid._≟_ natDecSetoid
>
> cSym : Symmetric _=c_
> cSym {infinity} {infinity} _    =  ⊤.tt
> cSym {infinity} {fin _}    x='y =  ⊥-elim x='y
> cSym {fin _}    {infinity} x='y =  ⊥-elim x='y
> cSym {fin m}    {fin n}    x='y  with m ≟ n
> ...                            | yes m=n = nSym m=n
> ...                            | no m/=n = ⊥-elim $ m/=n x='y
> ---------------------------------------------------------------
>
> I hoped for   cSym {fin m}  {.(fin m)} _  =  nRefl
>               cSym infinity .infinity  _  =  ⊤.tt
>
> to work - due to the type of the third argument.
> Buth all my `dot' variants are not type-checked.
>
> Thanks,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda


-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 490 bytes
Desc: PGP Digital Signature
Url : http://lists.chalmers.se/pipermail/agda/attachments/20130729/b230b29e/attachment.bin