Defining inductive types in intensional type theory purely in terms of type-theoretic data
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.