How to mechanically derive the recursor of a type from its constructors?

Question

In Martin-Löf Dependent Type Theory a type is commonly prescribed by how to construct its canonical terms and how to show that its canonical terms are definitionally equal. This means that the definition of a type contains no explicit information at all about its recursor / induction principle and how it should behave.

Am I right to suppose that, given the constructors of a type, we already have an implicit characterization of its recursor / induction principle – in the sense that there exists an algorithm that mechanically derives the recursor / induction principle of this type?

If this is correct I would like to know:

1. How such an algorithm look like? (References are fine)
2. How is this all related to Gentzen’s inversion principles?

Answer 1

Section 5.6 of the HoTT book discusses the general schema for inductive types, including how to get the corresponding induction principle.

In short, yes there is a general way to derive the elimination principle from the signature (the description of the construcotrs), and it is of course algorithmic. Coq does it, for instance, when you define an Inductive foo and it generates the eliminator foo_rect.