The Coq mailing list

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

Well, there seem to be two issues. The first one is about unique
choice, which I interpreted as hProp-truncation of A being a no-op
when A is an hProp. Currently, Coq has a Prop-truncation which is a
no-op (in the sense of supporting elimination to Type) when A is
syntactically a Prop-subsingleton (i.e. built from False, True, and,
Acc, eq). I was proposing to extend the current Prop-truncation into
an hProp-truncation, i.e. to extend the specific syntactic
Prop-subsingleton criterion into a full hProp-subsingleton
criterion. This extension would allow to make any provably-hProp
inductive definition into an impredicative hProp, i.e., explicitly,
because this would redefine Prop to mean hProp-truncation rather than
the current (weaker) syntactic Prop-truncation.

The second issue is about supporting impredicativity for all hProp,
including non-inductive types, i.e. for functional types. This is
actually a good question about which I'm unsure. What are the examples
of types in Type provably in hProp and whose conclusion is not already
an hProp (so that these functional types are not already put in Prop,
i.e., with the new criterion, in hProp)?

I may think for instance of "forall A:Type, A -> A" but how do you
prove that it is an hProp? Are there other candidates? If there are
actual examples, they would indeed escape the criterion allowing them
to support impredicativity.

Hugo

On Sun, Feb 28, 2021 at 01:37:50PM -0800, Michael Shulman wrote:
> 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?