The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

There is unique choice for Prop, which is called singleton
elimination, except that it applies only to a subset of hProp
syntactically recognizable as subsingleton, namely the subset
generated by "False", "True", "and", "Acc", and "eq" (up to "indices
matter"). [In passing, singleton elimination should actually be called
subsingleton elimination!]. I believe it would be no problems to add
an extra introduction rule for elimination to Type for any provably
subsingleton type and get full hProp unique choice, for instance, say,
with a declaration:

Subsingleton id params : ishProp A := proof.

for A an inductive type declared in Type so as to put it in Prop and
let it support impredicativity.

In addition to impredicativity, note that there would be a side impact
on program extraction (mentioned by Matthieu and Nicolas). Since
A:Prop is extracted to unit (and most of the time erased), to
implement singleton elimination, one need to provide a way to go back
from unit to (the simply-typed skeleton of) A. For A built from False,
True, Acc and eq, it is easy but for an arbitrary hProp, arbitrary
complex information would need to be rebuilt. So, this hProp-extended
Prop would have to be kept outside extraction erasure.

So yes, as far as I can judge, the above would provide an axiom-free
way to make hProp impredicative.

Best,

Hugo

On Sun, Feb 28, 2021 at 07:57:10AM -0800, Michael Shulman wrote:
> On Sun, Feb 28, 2021 at 4:58 AM Hugo Herbelin <Hugo.Herbelin AT inria.fr> 
> wrote:
> > In particular, not using Prop in the HoTT library is to my eyes more a
> > design choice than a real constraint.
> 
> This is true, but I would say it's a design choice of the HoTT/UF
> foundational system in general rather than of the HoTT/Coq library in
> particular.  The issue with Coq's Prop (as long as indices matter) is
> not its impredicativity, but the fact that it doesn't necessarily
> coincide with hProp.  In fact I believe there is no inclusion in
> either direction: types in Prop need not be h-props, and h-props need
> not even be equivalent to anything in Prop.
> 
> Using hProp as the basic notion of "proposition" in HoTT/UF is
> important for multiple reasons.  One is that it allows us to *prove*
> that some type is a proposition after the fact, versus how types in
> Prop must essentially be defined to be there when they are
> constructed.  Also, using hProp makes unique choice provable, without
> any axioms.  In fact this was one of the first points made by
> Voevodsky in his original development of his Foundations library: he
> was able to define an h-prop-valued "is finite" predicate and a
> "cardinality" function from finite types to nat, which could actually
> be evaluated to compute, for instance, the cardinality of bool * bool.
> 
> One could of course assert axioms making hProp equivalent to Prop,
> which semantically would amount to the axiom that the HoTT Book calls
> propositional resizing.  However, passing back and forth across these
> axioms would break the computable nature of unique choice.  I don't
> know how big an issue (if any) that would be for the HoTT/Coq library
> as it currently exists.
> 
> Is there any known axiom-free way to make hProp impredicative, or to
> make an impredicative Prop equivalent to hProp?