[Agda] Again, a question on records

[David Leduc]

> I'm not sure how Coq does it, either.

As far as I understand, Notations are untyped.
It's only when you apply them that Coq will fill the holes.
But you are saying that there are other legal ways to fill the holes, right?
But I claim that all these choices are equal.
Isn't it true in Agda too?

For example instead of the inferred t1
you could force the use of {| carrier := carrier t1 ; op := op t1 |}.

 Definition f (t1 t2 : T)(x1 y1: [t1])(x2 y2:[t2]) : [t1]*[t2] :=
   (op {| carrier := carrier t1 ; op := op t1 |} x1 y1, x2 $ y2).

But then is it easy to prove the following lemma:

 Goal forall t1 : T, t1 = {| carrier := carrier t1 ; op := op t1 |}.
 Proof.
 intros t1.
 destruct t1.
 trivial.
 Qed.