In ncat lab they say:

In type theory, induction-induction is a principle for mutually defining types of the form

`A:Type`

,and`B:A→Type`

, where both`A`

and`B`

are defined inductively, such that the constructors for`A`

can refer to`B`

and vice versa. In addition, the constructor for`B`

can refer to the constructor for`A`

. this sounds to me like mutual induction.

But then this post claims that induction induction is as powerful as induction recursion.

But then I know that induction recursion cannot be encoded in coq, so that means there has to be a difference betwen induction-induction and mutual inudction, but i cannot see it yet.

Last updated: Oct 04 2023 at 21:01 UTC