Feature: Accept some form of type ascriptions on data and codata

[alexkeizer]

In regular inductives, we can choose to explicitly give the universe:

inductive Wrap (α : Type 1) : Type 1
--                          ^^^^^^^^
  | mk : α → Wrap α

Currently, we blanket ban any type ascriptions, to prevent users from trying to define inductive families (which are fundamentally not supported).

We should allow a type ascription, and simply check it's of the form Type or Type u, where u may be a variable, an underscore (_), or a concrete universe level.

We could consider allowing arrows, as in Type -> Type -> Type as well, but this might be too confusing since it looks like how we would normally define inductive families.