The Coq mailing list

[Michael Shulman <shulman AT sandiego.edu>]

This is a cool idea!  I don't quite understand the suggested behavior
of the Subsingleton declaration.  E.g. you said that A is an inductive
type; is that essential?  Non-inductive types can also lie in hProp of
course.  And when you say "put it in Prop" what exactly would that do?

On Sun, Feb 28, 2021 at 12:13 PM Hugo Herbelin <Hugo.Herbelin AT inria.fr> wrote:
>
> 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?