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 theHProp
truncationfun A:Type => ∥A∥
, which assigns anHProp
to each typeA
. - Coq's new
SProp
. As far as I understand,SProp
is almost the same asHProp
, but instead of explicit rewrites, the type checker will be happy to implicitely convert any element of anSProp
into another. So I won't discussSProp
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 Prop
s are HProp
s. 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 Prop
s 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 ?
Prop
does not "collapse all theType_i
" because that would mean that it somehow makes them all equal. The correct phrase is "Prop
is closed under products indexed by abtirary types". $\endgroup$