[Agda] Again, a question on records

[David Leduc]

> However, I think in this case (records for mathematical structures) you
> could also work with the Agda module system. You can open a record like a
> module and work with the fields directly, so you have "carrier" and "op"
> already instantiated to a certain instance t of T.

But when I use more than one instance of a mathematical structure. I
want "op" be instantiated to the right one depending on its arguments.