It has been apparent in various PRs and CEPs that there are some open questions about how universes should work. So to start a discussion about some of the issues involved I want to propose the following and see what others think:

The sorts Prop, SProp and Type should all be polymorphic. That is there should be universe annotations for all of them. To retrieve the previous behaviour of one Prop and SProp, we would have a flag that enables prop resizing, allowing for a monomorphic behaviour on props. When this is disabled, Prop and SProp should live at the same universe level as Type. But this would also allow for subsingleton eliminators for Prop and SProp to be polymorphic.

Just some thoughts, curious what you think. cc @Pierre-Marie Pédrot @Hugo Herbelin

I also seem to recall some discussion of moving Prop closer towards behaving like hProp but I am not sure what the details are here.

I am confused by your proposal. My understanding is that universes are only meaningful in a predicative setting. Since `Prop`

is impredicative, I don't see much point in making it polymorphic. And if you are suggesting to make `Prop`

predicative, why would anyone still use `Prop`

instead of `Type`

? Because of proof irrelevance?

It is my understanding that the entire point of Prop is for erasure during extraction.

But I am suggesting that this can be done predicatively

Prop would be coq's hProp

but you could also have SProp which is not obtainable in a user defined way

Short answer: this subject is an emerging topic of research under the name "sort polymorphism" around here. This mechanism would extend the ability to quantify over indices to a quantification over arbitrary sorts.

There are a lot of issues, both theoretical (e.g. singleton elimination) and practical (e.g. unification).

Prop serves various purposes, included but not limited to: impredicativity / proof-irrelevance / erasure.

hProp is not Prop, it's incompatible with an erasable semantics.

Ali Caglayan said:

The sorts Prop, SProp and Type should all be polymorphic.

Pierre-Marie Pédrot said:

This mechanism would extend the ability to quantify over indices to a quantification over arbitrary sorts.

Is is possible that you are both taking about different things? Rethinking XProp as subtypes of `Type(α)`

, one `XProp(α)`

for each `α`

, with some specific property (such as subsingleton for hProp, being generated by 0, truncation and dependent function type for SProp - or something like that, being generated by 0, 1, /\, acc, eq, truncation and dependent function type for Prop, or something like that) for @Ali Caglayan and (I'm less sure though) a form of quantification over a discret set of sorts (such as both over current `SProp`

and the `Type`

s) for @Pierre-Marie Pédrot?

from a very practical point of view, `Prop`

is currently used as an indicator that the body of constant "should" be made opaque (thus saving memory, making parallel asynchronous proving possible, etc.)

for any changes to `Prop`

vs `SProp`

vs `Type`

, I think it's crucial to figure out what happens to the overall toolchain if big projects can/should suddenly make many of their constants transparent. In particular, I think there are already memory issues for UniMath due to avoiding `Qed`

@Karl Palmskog this is not completely true, we have the evergreen issue of Qed-opaque proofs of singleton types that might block when eliminating into Type.

Namely, eq and Acc.

Also you can perfectly put end proofs in Type with Qed. UniMath doesn't do that for other reasons.

(namely, why bother when any theorem can be stated as an equality)

completely agree that one can't have an iron-clad rule that (only) `Prop`

-sorted terms must (always) be opaque. I'm just saying that for better or worse, practitioners often use it as a rule of thumb.

in fact, figuring out the tradeoffs of making something opaque or transparent is arguably difficult for large projects. I was hoping to get erasure at the Coq level (instead of just in OCaml) via MetaCoq to do evaluation without getting stuck on `Acc`

or similar, but Matthieu said a while ago that they are not there yet.

from a proof engineering standpoint, `Qed`

is an extremely helpful abstraction barrier in that it allows you to edit a proof script with a near-guarantee that it won't break the rest of the project, which can be crucial when porting proofs to new versions of Coq. If everyone suddenly went UniMath, porting big projects without insider knowledge could easily become a nightmare.

would UniMath be better off in Agda anyway?

better: it seems that outside of (im)predicativity, that style of programming works better in Agda than Coq, and viceversa, and each is a local optimum

e.g. Agda doesn’t use Qed but it has much better affordances for writing “(sort-of) raw proof terms”, which is more convenient when you need precise control of definitional equalities.

a bit more helpfully (and I’ll stop the OT): if Coq wants to support that style, it might need so many changes it wouldn’t be Coq any more.

But a lot of people want to write "raw proof terms" using tactics. This is something agda cannot do.

But the discussion of Qed seems to be getting off topic.

There are a lot of issues, both theoretical (e.g. singleton elimination) and practical (e.g. unification).

Can we elaborate on these?

hProp is not Prop, it's incompatible with an erasable semantics.

Then isn't everything that is erasable also everything that is Qedable?

By erasable I mean that there is a realizability intepretation / extraction process where the type can be simply replaced by unit. It's pretty much unrelated to Qed-able because there are cases of the latter where the user knows how to retrieve a canonical computable instance out of a Qed proof, but extraction does not know that.

For instance, equality is erasable (if you assume UIP, which is the case in standard extraction) but you can't make it Qed except if you have e.g. decidable equality on the corresponding type

Same issue with Acc replacing UIP with some variant of Markov's principle.

Also another place where prop resizing came up was here: https://github.com/coq/ceps/pull/55

Last updated: Sep 09 2024 at 04:02 UTC