Defining inductive types in intensional type theory purely in terms of type-theoretic data To define a (non-indexed) W-type all we need is a type $A:U$ and a function $B:A\to U$ and we get a type $W_{a:A}B(a)$. To check that this definition is valid we only need to check that the definitions of $A$ and $B$ are valid.
Now general inductive types seem like very scary beasts and I still don't entirely understand what a proof checker kernel (e.g. in Coq) is doing to make sure the definition is valid.
In intensional type theory there is apparently a big gap between W-types and general inductive types. For example the generic W-type recursion applied to the W-type encoding of unary natural numbers is not as strong as standard recursion for natural numbers.
So the question is: is there a way to set up inductive types so that to check the validity of a definition you only need to check the validity of finitely many non-inductive typing judgements?
A strongly normalizing type theory can't fully interpret itself but I guess we could have a partially defined quote unquote specifically for the bits of data necessary to define inductive types. Can you suggest any references?
It turns out that $W$ types plus identity types (eq/= in Coq) allow you to construct pretty much all the general inductive types you want, with the expected computation rules, and even canonicity. This is a very recent result of mine, you can read a preprint at Why not W?, which has been accepted for publication in the TYPES 2020 post-proceedings.
The idea is that even though the standard construction of say the natural numbers from W types does not work, as is well known, a refined, slightly more complicated construction can be made to work. The way my refinement works is to use identity types to pick out the elements of the standard construction which are in canonical form.
This puts general inductive types on an internal, finitary footing, which is a large simplification of the theory. However, there remain some practical problems to be looked at around efficiency and usability.
Other, prior work on simplifying the theory of inductive types includes The Gentle Art of Levitation, by James Chapman, Pierre-Evariste Dagand, Conor McBride, and Peter Morris.