Stronger "induction" principles than induction-recursion

Question

Are there type theories in the literature with "induction" principles stronger than induction-recursion? This answer gives System F as an example of a theory stronger than MLTT + induction-recursion, but I'm interested in principles similar to ordinary induction and induction-recursion, not impredicativity.

Answer 1

Anton Setzer has work on type theories that are stronger than standard induction-recursion. In some ways, though, it's still in terms of simultaneous inductive and recursive definitions. The difference is in the intricacy and details of all the simultaneous definitions.

There are two papers that build up to and define this type theory. The first goes through 'normal' universes and up to Mahlo universes, which are the sort of universes Agda has, that are themselves closed under inductive-recursive definitions. Then the second goes beyond this, finally defining a "$Π_3$-reflecting universe," which I believe could also be called a "weakly compact" universe by analogy to large cardinal properties (similar to "Mahlo").

I only have a limited understanding of all this myself, but the idea goes something like this:

A starting point is the "Mahlo universe" which is a universe closed under inductive-recursive definitions. In some sense, this is like a universe closed under (standard) universe formation, because induction-recursion allows you to define types similar to the universe in ordinary Martin-löf type theory. So, a sort of 'obvious' next step is to try to define a universe that is closed under some amount of Mahlo-universe formation. You need to take care with this, though, because a universe both being Mahlo and having an inductive eliminator is contradictory. So, the method of definition has to be somewhat different than induction-recursion.

The idea introduced is to keep track of the "Mahlo degree" of universes. The degrees are well-founded trees, and a universe of Mahlo degree $d$ is closed under universes in a similar way to a Mahlo universe (e.g. for every map $F : \mathsf{ IFam}(\mathsf{U},\mathsf{El}) → \mathsf{IFam}(\mathsf{U},\mathsf{El})$, there is a universe $\hat{\mathsf{U}}_F : \mathsf{U}$ closed under $F$), but with the proviso that there is actually one $\hat{\mathsf{U}}_F^e$ itself of degree $e$, for each $e < d$. So, for $d = 0$ we get plain universes, containing no further universes, for $d = 1$ we get Mahlo universes. And the type of degrees is defined simultaneously with $\mathsf{U}$, so that 'new' values of $\mathsf{U}$ introduce new, larger degrees, similarly to an inductive-recursive definition.

The final step he takes to get to the $Π_3$ universe is to extend the notion of degree. Whereas before it was supposed to essentially be the same as $\mathsf{W\ U\ El}$, instead the degrees themselves are defined in a similar way to Mahlo universes. Essentially, $\mathsf{Deg}$ is now the inductive type with constructor:

$$\mathsf{deg} : (\mathsf{IFam}(\mathsf{U},\mathsf{El}) → \mathsf{Fam}_{\mathsf{Deg}}(\mathsf{U},\mathsf{El})) → \mathsf{Deg}$$

But, this is all still simultaneous with the definition of $\mathsf{U}$ and such.

If you find this unclear, even after studying the papers, I think you're probably in good company. I've tried formalizing something similar to the second-to-last step above in Agda, with some commentary. Setzer calls his construction the "autonomous Mahlo universe," because its Mahlo degree is given by the well-founded trees definable over itself. My formalization attempts to show that Agda's Mahlo universes are "autonomous super universes," where super universes are a weaker notion than Mahlo, that aren't contradictory when having an induction principle.

While writing this, I also tried extending the notion of degree in that file to the $Π_3$ one, and it seemed to work. I'm not sure what the result is, however. But you can try to work all this out in Agda to develop a better understanding of how things interleave. It's just that the 'degrees' are with respect to a fundamentally weaker notion of universe, because universes with an eliminator cannot themselves be Mahlo (if you try to write what such a thing would be, you will be rejected by Agda's positivity checker).

One thing to note, I suppose, is that it's difficult to see what one would do with these sort of universes (that can't already be done with less). Setzer is, in this work, primarily interested in understanding proof theory through the lens of type theory, so the ordinal-alike presentation is not much of a barrier in that respect. However, (large) induction-recursion has some pretty simple practical motivations, while I don't think the same can be said about a $Π_3$-reflecting universe. Perhaps there's some simpler notion similar to induction-recursion that is equivalent in power to $Π_3$-reflection, and seeing that would suggest more 'mundane' uses. But I don't think it's at all clear what that would be, just given the Setzer presentation.