Semantic definition of strict positivity for a functor
One semantic criterion is preservation of $\omega$-colimits, or $\omega$-cocontinuity. AFAIK, initial algebras of such functors correspond to finitary inductive types in type theory. The construction of initial algebras, given by Adámek's theorem, can be formalized inside type theory as well. It's described in this paper and there's a Coq formalization for it. Probably there is a generalization of this to transfinite colimits, which would give us infinitary inductive types, but for this I don't know any formalization.