This is a bit theoretical question. We can define fx but seemingly not fx':
Function fx {A} (x:A) (f:A->Type) (g:Type->f x): f x := g (f x).
Definition fx' {A} (x:A) (f:A->Type): f x.
In a way, this makes sense, as one cannot prove from the f and x that f has been (or will be) applied to x. But we can apply f to x to get something of type Type:
assert (h := f x).
This seems puzzling: one can apply f to x but still can't obtain a witness y: f x that he has done so.
The only explanation I can think of is this: as a type, f x is an application, as a term, it's just a type. We cannot infer a past application from a type; similarly, we cannot infer a future application from a function and its potential argument. As for (the instance of) applying itself, it isn't a stage in a proof, so we cannot have a witness of it. But I'm just guessing. The question:
Is it possible to define fx'? If yes, how; if no, why (please give a theoretical explanation)
First, a direct answer to your question: no, it is not possible to define fx'. According to your snippet, fx' should have type
forall (A : Type) (x : A) (f : A -> Type), f x.
It is not hard to see that the existence of fx' implies a contradiction, as the following script shows.
Section Contra.
Variable fx' : forall (A : Type) (x : A) (f : A -> Type), f x.
Lemma contra : False.
Proof.
exact (fx' unit tt (fun x => False)).
Qed.
End Contra.
What happened here? The type of fx' says that for any family of types f indexed by a type A, we can produce an element of f x, where x is arbitrary. In particular, we can take f to be a constant family of types (fun x => False), in which case f x is the same thing as False. (Note that False, besides being a member of Prop, is also a member of Type.)
Now, given your question, I think you are slightly confused by the meaning of types and propositions in Coq. You said:
This seems puzzling: one can apply
ftoxbut still can't obtain a witnessy: f xthat he has done so.
The fact that we can apply f to x simply means that the expression f x has a valid type, which, in this case, is Type. In other words, Coq shows that f x : Type. But having a type is a different thing from being inhabited: when f and x are arbitrary, it is not possible to build a term y such that y : f x. In particular, we have False : Type, but there is no way we can build a term p with p : False, because that would mean that Coq's logic is inconsistent.