[Agda] deriving Eq for Agda?

[Julian Beaumont]

As far as I know theres no equivalent for these in agda, however, you
might be interested in the following paper:

A Universe of Strictly Positive Families
http://www.cs.nott.ac.uk/~pwm/papers/ijfcs.pdf

It presents a universe for strictly positive families in epigram and
shows how to implement a number of operations for types in this
universe, including equality. Translating the proofs to agda should be
fairly simple. To define these operations for a new inductive type in
agda you would need to define a bijection between your type and the
corresponding type in this universe. If all you want is a single
operation, for example equality, this is probably just as much work as
implementing the operation directly. If, however, your interested in
multiple operations that can be defined generically for all inductive
type, for example equality and map, than it may be beneficial to
define the bijection and use the generic versions.

Disclaimer: I haven't attempted to use this approach and don't know
how practical it would be. It would probably be much more useful if
agda could automatically define the translation to/from the universe
for inductive types.

P.S. Sorry if this comes through twice, I accidentally send from the
wrong email the first time and canceled it.

2009/12/3 Vilhelm Sjöberg <vilhelm at cis.upenn.edu>:
> Dear Agda list,
>
> in Haskell I can say "deriving Eq" and in Coq "decide equality". Is there a
> similar automated tool for creating equality decision procedures for Agda
> inductive types?
>
> Failing that, is there a recommended idiomatic way of writing them, and do you
> know of any elegant examples? Each time I've tried to write one it seems quite
> ungainly and ad-hoc.
>
> Thanks,
>  Vilhelm
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>