What types are propositions?

Question

In the propositions-as-types paradigm, we are still faced with the question : what types are propositions ? I currently know 3 different answers :

• Coq's sort Prop and its typing rule that asserts it is closed under products indexed by abtirary types $$\frac{A : \mathsf{Type}_i \qquad x : A \vdash B(x) : \mathsf{Prop}} {\prod_{x : A} B(x) : \mathsf{Prop}}$$
• HoTT's HProp, which are types where all elements are equal, together with the HProp truncation fun A:Type => ∥A∥, which assigns an HProp to each type A.
• Coq's new SProp. As far as I understand, SProp is almost the same as HProp, but instead of explicit rewrites, the type checker will be happy to implicitely convert any element of an SProp into another. So I won't discuss SProp anymore here.

I see some common points between Prop and HProp, the main one being that Coq is compatible with the axiom of proof irrelevance, which asserts that all Props are HProps. Also there is the similar guarded match. Coq accepts to destruct a proof of a Prop only when it is proving a Prop. Likewise, the recursion principle of the HProp truncation accepts to lift ∥A∥ -> B into A -> B, only when B is an HProp. Another common point is seen via Coq's extraction mechanism : all proofs of Props will be discarded, because they map to singleton types.

However I don't clearly see how either of these definitions captures the concept of a proposition. A HProp makes some sense to me, because uniqueness allows to interpret inhabitants as mere proofs that the HProp is true. But then one can argue that a proposition does have different proofs, some being simpler than others for example. Or some using more or less axioms than others (constructive proofs versus classical proofs for instance). Concerning Coq's Prop, I understand that it is impredicative, but I don't think it explains enough. And why didn't Coq take proof irrelevance as a hard typing rule (where 2 proofs are the same Prop would be judgementally equal, rather than propositionally equal) ? I think it would be compatible with HoTT, if we redefine eq in sort Type rather than Prop.

Part of the answer might come from the function extensionality axiom. If it is not there, then it is very hard to prove that a type is a HProp. So Coq's Prop might be a way to handle propositions without assuming funext. For instance, the closure of HProp by the forall quantifier needs funext, so Prop's typing rule might be seen as an instance of funext.

Are there other definitions of propositional types ?