# Implicit argument resolution

Hi all,
I am perplexed by this piece of Coq code, which defines the bijectivity of a function:

``````Definition injective {A B} (f : A -> B) := forall x y : A, f x = f y -> x = y.
Definition surjective {A B} (f : A -> B) := forall y : B, exists x, f x = y.
Definition bijective {A B} (f : A -> B) := injective f /\ surjective f.

Definition idf {A} (x : A) := x.

Lemma id_bij {A : Type} : bijective idf.
``````

Coq dismisses this because it cannot find an instance for the `B : Type` in bijective. However, the identity function has type `A -> A`, i.e. I want Coq to understand that in this case, `A = B`. Is there any way to avoid explicit argument passing using @ ?

Best,
MRandl

I am not sure it is really about understanding that `A = B`. I think both `A` and `B` are unknown: nothing tells us which `A` has to be considered as implicit argument of `idf` in the statement of `id_bij`.
Why do you think Coq should be able to infer it?
`Lemma id_bij {A : Type} : bijective (@idf nat).` is accepted.
`Lemma id_bij {A} : bijective (@idf A).` is accepted.
There does not seem to be a reason why Coq should choose one rather than the other.

I think the confusion in the original question comes from the fact that two bound variables seemingly have the same name `A`. Therefore, a human user might believe that they are somehow related, but they are really different. The definition `Definition idf {A} (x : A) := x.` really has the same meaning has `Definition idf {C} (x : C) := x.` and in this case one is less drawn to think that the `A` in `id_bij` should be the same as the `C` in `idf`.

Ah yes, I see.
Thanks a lot to both of you!