Deep Induction for Inductive Families
摘要
Deep induction provides induction rules for deep data types, i.e., data types that are defined over, or mutually recursively with, (other) such data types. Deep induction is currently defined only for type-indexed types, such as ADTs, nested types, and GADTs. In this paper we show how to extend deep induction from data types with only type indices to data types with term indices as well. Specifically, we extend to inductive families—as found in dependently typed systems such as Agda, Epigram, and Idris—the methodology for deriving sound deep induction rules that was originally developed for nested types and has recently been extended to GADTs.