pEmpty : Sort u

[kbuzzard]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

We don't seem to be able to make a Sort u-valued inductive empty type right now.

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
-/

It is possible to do this in Lean 3. I personally am slightly unclear about the use of this type, but I noticed it when porting Lean 3 files to Lean 4 so thought I'd mention it.

[leodemoura]

It has been added to the Init package. It is called PEmpty.