Matthieu gave at the Coq workshop examples of use of qualities (thanks!). If I understand correctly, when the quality is SProp
, Prop
or Set
, as was asked, the levels are irrelevant. Would it then make sense to simplify the notation, such as, I don't know, being able to only write this:
Set Universe Polymorphism.
Definition id@{ s | u | } (A:Type@{s|u}) (x:A) := x.
Check id@{Prop}.
or that:
Check id@{Prop|}.
Set is not a quality
Type is a quality
Would it then make sense to simplify the notation, such as, I don't know, being able to only write this:
finding which levels are irrelevant when a quality is impredicative in general requires unfolding the definition
so I'm not sure what the precise meaning of such a notation would be
Set is a universe of the Type quality (at the bottom)?
Yep, Set = 0
Set is a universe level, which other levels are generally declared to be >= Set (except while checking template poly inductives)
Set is also a notation for Type@{Set}
probably we should rename the level to 0
Hugo Herbelin said:
Matthieu gave at the Coq workshop examples of use of qualities (thanks!). If I understand correctly, when the quality is
SProp
,Prop
orSet
, as was asked, the levels are irrelevant. Would it then make sense to simplify the notation, such as, I don't know, being able to only write this:Set Universe Polymorphism. Definition id@{ s | u | } (A:Type@{s|u}) (x:A) := x. Check id@{Prop}.
or that:
Check id@{Prop|}.
That's also my main gripe with our handling of impredicative universes. It also shows up as "universe foo is unbound" during elaborations when one would have expected the universe to be set as 0 as you've been using Prop. However there does not seem to be an evident solution to that.
In the quality model, is there a place for subsingleton types, such as hProp or subsets of hProp such as (a predicative) Prop, i.e. a place where we can make a predicative form of Prop live (up to ensuring a truncation).
finding which levels are irrelevant when a quality is impredicative in general requires unfolding the definition
It can probably be an information attached to the universe signature of the constant?
You could analyse that u is only used with s, if all uses of u are linked with s = Prop | SProp, and u has no constraint, it could heuristically be set to 0, no?
At the very least, _
could be accepted for an irrelevant level. (Or perhaps it already is?)
And after testing, it actually is, which seems like a better style than writing foo
everywhere.
In the quality model, is there a place for subsingleton types?
Maybe this is a wrong question as it is about h-level rather than size.
And after testing, it actually is, which seems like a better style than writing
foo
everywhere.
I tested too and it seems to generate a new universe at each new application.
In any cases, that was a very nice talk. I'll continue thinking about it offline.
_
is a hole regardless of if it's a term or a universe
leftover term holes produce an error ("cannot infer placeholder" etc)
leftover universe holes become new universes, except when using @{...}
without +
in which case they produce an error ("unbound universe")
Last updated: Oct 13 2024 at 01:02 UTC