[Agda] Something like type classes in Agda?

[Dirk Ullrich]

Hallo,

can implement or fake something like type classes in Agda?

A simple example: I can implement, for instance, a product binary type
either by using `data' or `record'. I can put these implementations in
different modules but give them the same 'API' - say `_x_' for the
type constructor, `<_,_> for the pairing and `pr0', `pr1' for the
projection function. Now I do not want to care whose of these modules
I use in other modules that need binary products.

Dirk