Can I assume that if `t : I@{u1 .. un}`

for `I`

universe polymorphic niductive, then if `t`

is a constructor `k`

it is `k@{u1 .. un}`

?

Do the inductive type and its constructor agree on universe instances?

if cumulative polymorphic then no

unless I misunderstand the question

Last updated: May 28 2023 at 13:30 UTC