Tootfinder

I've been reading the paper on small induction-recursion (which is really well-written btw!) and I think there might be a similar kind of terminological thingy about induction-recursion as with the "type-theoretic axiom of choice".
For context, "type-theoretic axiom of choice" is an old name for the distributivity of Π over Σ, which has nothing to do with choice. The reason it's named that is that, if you interpret ∀ as Π and ⊃ as Σ, the formulation of the axiom of choice in terms of relations
(∀ (x : X). ⊃ (y : Y). R(x, y)) − (⊃ (f : X − Y). ∀ (x : X). R(x, f(x)))
is just the distributivity of Π over Σ, which is trivial. The real mathematical content of the axiom of choice in type theory comes from the distributivity of Π over the propositional truncation, since the correct interpretation of ⊃ x. P x is ⊥ Σ x. P x ⊥.
Similarly, "induction-recursion" is made up of two parts: small induction-recursion, which is equivalent to indexed inductive definitions and thus rather anodyne, and the resizing of those definitions so that they live in U when they should live in U⁺, which is where the expressive power of IR comes from.
So, while "type-theoretic axiom of choice" is a very strong name for something innocuous, "induction-recursion" is an innocuous name for something very strong, essentially for dual reasons.
I hope this is not too obvious; I sure wish someone had explained this to me the first time I learned about induction-recursion.