In ncat lab they say:
In type theory, induction-induction is a principle for mutually defining types of the form
B:A→Type, where both
Bare defined inductively, such that the constructors for
Acan refer to
Band vice versa. In addition, the constructor for
Bcan 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