Well-formedness condition for inductive types I work on implementing a simple dependently typed language. I want to implement inductive types there. However, I want them to be well formed. From what I've seen in Coq not all types are acceptable. What can I read about them? Could give a simple enough well-formedness condition which I can use?
Inductive types have been studied heavily and many variants exist. A well-known introduction to inductive definitions is


P. Aczel, An Introduction to Inductive Definitions


which was originally published in the indispensable Handbook of Mathematical Logic, but is now available online stand-alone. An introduction to inductive types is


T. Coquand, P. Dybjer, Inductive Definitions and Type Theory: an Introduction.


The theory of inductive definitions for Coq was first (?) approached in


F. Pfenning, C. Paulin-Mohring, Inductively defined types in the Calculus of Constructions,


I don't know to what extend modern Coq has diverged from what's described in that paper. Either way, none of those is easy reading. You're probably better off to look at a Coq manual and copy the well-formedness conditions imposed there.