Strongly normalizing type theory beyond induction-recursion Are there known type theories in the literature, which have strong normalization proofs and their proof-theoretical strength goes beyond strength of type theories with induction-recursion?
Yes. System F is probably the simplest example. As far as I know, you can’t prove normalisation for it in a dependent type theory with induction-recursion — you need at least impredicative prop to do so.