Subtyping in Coq

Question

I defined Subtype as follows

Record Subtype {T : Type} (P : T -> Prop) := {
    subtype       :> Type;
    subtype_inj   :> subtype -> T;
    subtype_isinj : forall s t : subtype,
      (subtype_inj s = subtype_inj t) -> s = t;
    subtype_h     : forall x : T, P x -> (exists s : subtype,x = subtype_inj s);
    subtype_h0    : forall s : subtype, P (subtype_inj s)
  }.

Can the following theorem be proven?

Theorem Subtypes_Exist : forall {T} (P : T -> Prop), Subtype P.
forall (T : Type) (P : T -> Prop), Subtype P

If not, is it provable from any well-known compatible axiom? Or Can I add this as an axiom? Would it conflict with any usual axiom? (like extensionality, functional choice, etc.)

Answer

Your definition is practically identical to the one of MathComp; indeed, what you are missing mainly is injectivity due to proof relevance.

For that, I am afraid you will need to assume propositional irrelevance:

Require Import ProofIrrelevance.

Theorem Subtypes_Exist : forall {T} (P : T -> Prop), Subtype P.
forall (T : Type) (P : T -> Prop), Subtype P
Proof.
forall (T : Type) (P : T -> Prop), Subtype P
  intros T P; set (subtype_inj := @proj1_sig T P).
T: Type
P: T -> Prop
subtype_inj:= proj1_sig (P:=P): {x : T | P x} -> T
Subtype P
  apply (@Build_Subtype _ _ { x | P x} subtype_inj).
T: Type
P: T -> Prop
subtype_inj:= proj1_sig (P:=P): {x : T | P x} -> T
forall s t : {x : T | P x},
subtype_inj s = subtype_inj t -> s = t
T: Type
P: T -> Prop
subtype_inj:= proj1_sig (P:=P): {x : T | P x} -> T
forall x : T,
P x -> exists s : {x0 : T | P x0}, x = subtype_inj s
T: Type
P: T -> Prop
subtype_inj:= proj1_sig (P:=P): {x : T | P x} -> T
forall s : {x : T | P x}, P (subtype_inj s)
  +
T: Type
P: T -> Prop
subtype_inj:= proj1_sig (P:=P): {x : T | P x} -> T
forall s t : {x : T | P x},
subtype_inj s = subtype_inj t -> s = t intros [s Ps] [t Pt]; simpl; intros ->.
T: Type
P: T -> Prop
subtype_inj:= proj1_sig (P:=P): {x : T | P x} -> T
t: T
Ps, Pt: P t
exist (fun x : T => P x) t Ps =
exist (fun x : T => P x) t Pt
    now rewrite (proof_irrelevance _ Ps Pt).
  +
T: Type
P: T -> Prop
subtype_inj:= proj1_sig (P:=P): {x : T | P x} -> T
forall x : T,
P x -> exists s : {x0 : T | P x0}, x = subtype_inj s now intros x Px; exists (exist _ x Px).
  +
T: Type
P: T -> Prop
subtype_inj:= proj1_sig (P:=P): {x : T | P x} -> T
forall s : {x : T | P x}, P (subtype_inj s) now intro H; destruct H.
Qed.

You can always restrict you predicate P to a type which is effectively proof-irrelevant, of course.