pEmpty

Stream: lean4

[Kevin Buzzard]

inductive pEmpty : Sort u
/-
invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0),
  but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u'
  u
-/

Works fine in Lean 3. This inductive pEmpty : Type u works fine in Lean 4 but is there a way of leaving Prop open as a possibility?

[Daniel Selsam]

FYI there is a similar restriction in Lean3 but apparently only for structures:

structure foo : Sort u
/-
invalid universe polymorphic structure declaration,
the resultant universe is not Prop (i.e., 0),
but it may be Prop for some parameter values (solution: use 'l+1' or 'max 1 l')
-/

[Daniel Selsam]

FYI there is also a 5-year-old TODO to generate two recursors for such inductives: https://github.com/leanprover-community/lean/blob/master/src/kernel/inductive/inductive.cpp#L321-L322

[Mario Carneiro]

Because this is a large-eliminating type, it would actually be fine to have a Sort u inductive here. The kernel will accept the type and produce the right result, but the elaborator has the wrong heuristic and is rejecting the type

[Daniel Selsam]

Yes, I think the elaborator check is unnecessarily aggressive in this case. @Kevin Buzzard I suggest you create an issue for this.

[Mario Carneiro]

The same comment applies to Sort u structures

[Mario Carneiro]

as long as the inductive specification is large-eliminating, you can do the obvious thing to construct the projections

[Mario Carneiro]

(concretely, that means that a structure with no fields or with only Prop fields can live in Sort u)

[Kevin Buzzard]

lean4#537

[Gabriel Ebner]

You could also take a leaf out of the core Lean book and disable the check:

set_option bootstrap.inductiveCheckResultingUniverse false in
inductive PUnit : Sort u where
  | unit : PUnit