[Agda] Again, a question on records

[David Leduc]

Thank you for your explanation, Dan.
But I want that the infix notation _$_ works for all record of type T.
More precisely, how can I translate the following Coq code in Agda?

Record T : Type := {
  carrier : Set ;
  op : carrier -> carrier -> carrier
}.

Notation "[ t ]" := (carrier t).

Notation "x $ y" := (op _ x y) (at level 50, left associativity).

Definition f (t1 t2 : T)(x1 y1: [t1])(x2 y2:[t2]) : [t1]*[t2] :=
  (x1 $ y1, x2 $ y2).

You see here that the right record is inferred from the types of xi and y1.