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 ?

Answer 1

The original conception of propositions-as-types did not distinguish propositions and types at all: all types are propositions. Under this view, we may indeed speak of different proofs of a proposition.

One way to understand the differences between different conceptions of propositions-as-types is to view them as capturing different notions of provability and truth:

• If we say that Prop = Type then the elements of a proposition are the proofs, so we are capturing proof constructions. We may analyze proofs, and for instance distinguish them according to their size, the assumptions they use, etc.

• If we say that Prop = HProp then the elements of a proposition witness existence of proofs (but are not specific proofs), so we are capturing provabillity. We can still discern the reason for a proposition being true, because we can analyze the proof as lons as further constructions do not depend on the choice of proof.

• If we use the strict SProp which makes all proofs judgmentally equal (or simply erases proof altogether), then inside type theory we can never "discern" the reasons for a proposition being true, so this is more like truth, i.e., an external reason for something being the case. We do have soundness in the sense that type theory can express semantic entailment, e.g., if $p$ and $q$ are true then so is $p \land q$.

Coqs Prop is conservative in the sense that it makes no commitment as to what Prop is supposed to be. Coq is compatible with the view that Prop is an (impredicative) Type, as well as that it is something like HProp, or even just bool. This is a design decision.