[Agda] Again, a question on records

[Benja Fallenstein]

Hi David,

On Mon, Sep 20, 2010 at 5:00 AM, David Leduc
<david.leduc6 at googlemail.com> wrote:
> 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 |}.

But what about {| carrier := carrier t1 ; op := fun x y => x |}?

- Benja