With the following definition:
Inductive eq (A : Type) (x : A) : A → Prop := eq refl : (eq x) x
Parameter a b : A.
When I consider one of its instance eq a b, I read (eq a) of type A -> Prop.
Then, my question is that how (eq a) b can establish the fact that a and b corresponds to the same object?
The strange thing to me is that we have no information about what does (eq a) actually do.
To add to John's answer, people seem to appreciate the informal description I gave here of how I think intuitively of indexed type families:
https://stackoverflow.com/a/24601292/553003
I would also add that there is a distinction between the type (eq a) b (which is the same as eq a b), and a term that has this type.
For instance, you can define:
Definition a_weird_type : Type := eq 0 42.
Because such a type is just a statement without a proof. You should not be able to define a_weird_term that has type a_weird_type though, because you will never convince the system that 0 and 42 are actually equal.
Note that there is still a little bit of checking though, so you cannot define:
Definition a_weirder_type : Type := eq 42 true. (* Coq will reject this *)
Because the eq type implicitly carries the type of the elements it compares, and the type system will ensure that the two elements have that type:
Check (@eq nat 42 true).
(* ^^^^ this should have type nat *)
Check (@eq bool 42 true).
(* ^^ this should have type bool *)
Check (@eq nat 23 42).
(* fine, but not provable *)
Eq a is a predicate that is only defined (only has the inhabitant eq_refl) if its argument is equal to b, where equality means "up to unification by the typechecker". So a has to be seen by Coq to be the same as b, otherwise Eq a b is equivalent to False.
