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
.
map_f : (A -> B) -> F A -> F B
. What more do you need? $\endgroup$