Most theorem provers simply axiomize inductive types (or equivalently W types) in the abstract which is fine.
But I'm curious about explicit constructions of inductive types within the theory.
I suppose I'm interested in both inductive types and "weak inductive types" (weak initial algebras) such as impredicative encodings. I think the term I've most found in my searches has been "weak natural numbers object." Inductive types can be better but weak inductive types are cool too.
I know you can use impredicative universes as in System F to encode inductive types. Or you can just accept a universe bump. And apparently if you internalize a small amount of parametricity you can construct appropriate induction principles.
But I'm pretty sure I've heard you can construct inductive types other ways. I think maybe you need to assume some classical principles? I've read some stuff on transfinite induction I still don't really get. I think once you have a base inductive type of ordinals you can construct other inductive types in those terms?
I have a hunch you can abuse impredicative proof irrelevant propositions and natural numbers to construct inductive types but I don't really have anything solid here.
Also for some reason I think it's easier to construct free monads the hard way instead of inductive types? I'm not sure this is an important issue.
I don't think W types and polynomial endofunctors directly solve the problem. They provide some clarifying language for how to talk about inductive types but they're not quite an explicit construction.
There's a paper "Induction Is Not Derivable in Second Order Dependent Type Theory" I don't understand yet but I think all this means is you need to assume more axioms than second order dependent type theory?