Stream: Coq users

Topic: What is the difference between ind-ind and mut-ind

walker (Apr 12 2023 at 07:55):

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