Well-formedness condition for inductive types
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.