Strong induction for higher-inductive types? › Background [01G6]

An inductive datatype comes with a primitive induction rule, which allows you to make recursive calls on immediate recursive subterms of the constructors. For more sophisticated kinds of recursion, in which you may make a recursive call on a deeper subterm, you need to define a separate induction principle; for natural numbers, this is often called strong induction.

One way to handle this generically for inductive datatypes \(D\) is to define for each family \(x:D\vdash P[x]\) a new family \(x:D\vdash \mathsf {Memo}_D^P[x]\) that consists of the instances of \(P\) at all elements strictly below \(x\) in the structural order. For example:

\[ \begin {aligned} &\mathsf {Memo}_{\mathbb {N}}^P[0] :\equiv \mathbf {1}\\ &\mathsf {Memo}_{\mathbb {N}}^P[n+1] :\equiv \mathsf {Memo}_{\mathbb {N}}^P[n]\times P[n] \end {aligned} \]

This particular description comes from Conor Titania Mc Bride’s PhD thesis. Then a recursion combinator is given that only makes the induction hypotheses available without splitting on anything just yet:

\[ \mathsf {Rec}_D^P : ((x : D) \to \mathsf {Memo}_D^P[x] \to P[x]) \to ((x : D) \to P[x]) \]

Then a separate non-recursive dependent case analysis principle \(\mathsf {Case}_D^P\) is given. These two principles employed together give a flexible foundation for structurally recursive dependently typed programming.