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:
- How such an algorithm look like? (References are fine)
- How is this all related to Gentzen’s inversion principles?