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