<p><a href="https://books.google.si/books?id=LkDUKMv3yp0C&amp;lpg=PP1&amp;pg=PA164#v=onepage&amp;q&amp;f=false" rel="nofollow noreferrer">Section 5.6 of the HoTT book</a> discusses the general schema for inductive types, including how to get the corresponding induction principle.</p>

<p>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 <code>Inductive foo</code> and it generates the eliminator <code>foo_rect</code>.</p>

CC BY-SA 4.0
2018-11-20T12:47:52.317Z
Or doing pattern matching of inductive types in Agda.
Jonathan Prieto-Cubides
CC BY-SA 3.0
2017-04-09T10:31:52.483Z
2017-04-09T10:31:52.483Z
Andrej Bauer
<p>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. </p>

<p>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 <em>there exists an algorithm that mechanically derives</em> the recursor / induction principle of this type?</p>

<p>If this is correct I would like to know:</p>

<ol>
<li>How such an algorithm look like? (References are fine)</li>
<li>How is this all related to <a href="https://plato.stanford.edu/entries/proof-theoretic-semantics/#InvPriHar" rel="noreferrer">Gentzen’s inversion principles</a>? </li>
</ol>

CC BY-SA 3.0
2017-04-10T07:33:04.297Z
Cf. Peter Dybjer's [Inductive Families](https://link.springer.com/article/10.1007%2FBF01211308?LI=true)
gallais
<lo.logic><type-theory><dependent-type>
How to mechanically derive the recursor of a type from its constructors?
StudentType
# How to mechanically derive the recursor of a type from its constructors?

(Asked by: username_0 on 2017-04-09)

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](https://plato.stanford.edu/entries/proof-theoretic-semantics/#InvPriHar)?

**Tags:** lo.logic, type-theory, dependent-type

> **Comments:**
> **username_1**: Cf. Peter Dybjer's [Inductive Families](https://link.springer.com/article/10.1007%2FBF01211308?LI=true)  

---

## 1 answers

### Answer by username_2 on 2017-04-09. Score: 3

[Section 5.6 of the HoTT book](https://books.google.si/books?id=LkDUKMv3yp0C&lpg=PP1&pg=PA164#v=onepage&q&f=false) 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`.

> **Comments:**
> **username_3**: Or doing pattern matching of inductive types in Agda.  

---

