On 18 December 2017 at 08:04, Michael Shulman <shu...@sandiego.edu> wrote:

> It sounds like Lean
> probably doesn't have this problem, i.e. if you define an inductive
> *type* then it is always a type and never turns out to be a
> proposition?


Exactly. If you ask an inductive type to be in Type, it will never end up
in Prop. If you want an inductive type to be in Prop, then you have to tell
that explicitly. You can do that for any inductive declaration, but in the
cases where singleton elimination doesn't hold, the generated induction
principle will only eliminate to the universe Prop.