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: Feb 05 2023 at 23:30 UTC