The Coq mailing list

[Ambrus Kaposi <kaposi.ambrus AT gmail.com>]

On Tue, Jun 12, 2018 at 2:52 PM Carmine Abate 
<carmine.abate AT inria.fr>
 wrote:
> Formally my question can be formulated as
> " given an inductive type \alpha, (like the one I wrote previously)
>   what is its induction principle \alpha_ind?

For this first part of your question, we have a paper describing an
algorithm to generate the types of induction principles for an
inductive type given by its sort(s) and list of constructors.

  Ambrus Kaposi and András Kovács, A Syntax for Higher
Inductive-Inductive Types, FSCD 2018
  https://akaposi.github.io/hiit.pdf

It works for a general class of inductive types as it includes
inductive-inductive types and higher inductive types.

>   and what is a term with type \alpha_ind? "

This is usually done using a general combinator such as fixpoint in
Coq. We haven't done this part yet.