A large class of inductive-recursive definitions, including the above, can be captured by a general schema (Dybjer 2000) which extends the schema for inductive definitions mentioned above. As shown by Setzer, intuitionistic type theory with this class of inductive-recursive definitions is very strong proof-theoretically (Dybjer and Setzer 2003). However, as proposed in recent unpublished work by Setzer, it is possible to increase the strength of the theory even further and define universes such as an autonomous Mahlo universe which are analogues of even larger cardinals.