Stack Exchange network consists of 183 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.
You should write "inductive type" or "inductive family" instead of "induction-recursion". That means something else. None of your examples here are inductive-recursive.
"and everybody can talk about terminal coalgebras without knowing about coinduction": I don't get this comment, reasoning by coinduction is usually defined to mean reasoning from the existence and universal properties of some terminal coalgebras.
Transfinite universe hierarchies are completely fine, they are usually not considered because countable universes is enough for most practical purposes. The ordinal notation convention would be more appropriate, since universe levels must be ordered, so we'd write $\omega_0$. If we have $U_{\omega_0}$, that enables quantification over all finite levels.
