Coq: defining a function from a sigma type to its second projection (and making it a coercion)

Question

I have trouble proving the type of the second projection from a sigma type:

Variable X:Type.
Variable Phy: X -> Type.
Definition e {x:X}: {x:X & Phy x} -> Phy x. 
intro. Fail exact (@projT2 _ _ X0).
(*The term "projT2 X0" has type "Phy (projT1 X0)"
while it is expected to have type "Phy x" (cannot unify
"(fun x : X => Phy x) (projT1 X0)" and "Phy x").*)

Is it the case that having a witness of {x:X & Phy x} (or {x:X | Phy x}) is insufficient for obtaining a witness of Phy x via projections? Either way, I could define e (more stupidly) by assuming the witnesses. Furthermore, I want to make it a coercion (but fail):

Reset e.
Definition PhyX := {x:X & Phy x}.
Definition e {x:X} {z:Phy x} {y:PhyX}: PhyX -> Phy x := fun y => z.
Coercion e: PhyX >-> Funclass. (*e does not respect the uniform inheritance condition*)

Now to the question: Can I define e more sensibly and/or make it a coercion?

EDIT: I suppose assuming a witness of Phy x is necessary because of the way existT is declared: existT (x:A) (_:P x). Here's a better version of the 2 last lines of code above (still couldn't make it a coercion):

Definition e {x:X} {h:Phy x}: PhyX -> Phy x := fun _ => projT2 (existT _ _ h).
Coercion e: PhyX >-> Phy. (*e does not respect the uniform inheritance condition*)

Answer 1

In your definition, there are two X values: the one given as an argument with {x:X}, and the one hidden in the sigma. These two are not interchangeable.

What you can do is this:

Definition e (p : {x:X & Phy x}) : Phy (projT1 p).
  destruct p; simpl; assumption.
Defined.