Semantic definition of strict positivity for a functor

Question

If we consider a definition of recursive type as:

F : Type -> Type;
T = fix F;

It is customary to talk about the functor F needing to be positive or strictly positive in order to avoid non-termination in the recursor.

I'm familiar with the usual syntactic definition of strict positivity, but I'm looking for corresponding semantic definitions, especially ones that can be expressed in the system (rather than being defined at the meta level).

The closest I have found is the work on containers (Abbott et.al., 2005), but it appears to require some "creativity" to come up with a container corresponding to a given functor and then prove equivalence between the two. I'm looking for something that talks more directly about the properties of F.

Answer 1

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.