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 collapses all`Type_i`

universes $ $ \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 `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 ?