In terms of categorical semantics, an inductive type is a type whose interpretation is given by an initial algebra of an endofunctor. (from nLab)

References:
nLab
Wikipedia
Lean
Coq