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.