Intuition Behind Strict Positivity?
It sounds like you want an overview of normalization arguments for type systems with positive datatypes. I'd recommend Nax Mendler's PhD dissertation: http://www.nuprl.org/documents/Mendler/InductiveDefinition.html.

As the date suggests, this is pretty classic work. The basic intuition is that an ordinal $\lambda$ can be associated to any element of a positive inductive type, e.g. for the data type

Inductive Ord = Zero : Ord | Suc : Ord -&gt; Ord | Lim : (Nat -&gt; Ord) -&gt; Ord

We would get:

$$ \lambda(t) = 0$$
if $t$ is a normal form which is not a constructor
$$ \lambda(\mathrm{Zero}) = 0$$
$$ \lambda(\mathrm{Suc}(o)) = \lambda(o)+1$$
and
$$ \lambda(\mathrm{Lim}(f)) = \sup_n \lambda(f\ n)$$

where $n$ ranges over terms with normal forms. The caveat is that this interpretation is only defined in the 3rd case when $f\ n$ has a normal form as well, which requires some care in the definitions.

One can then define recursive functions by induction over this ordinal.

Note that these data types can be defined already in classical set theory, as indicated in the excellent Inductive Families paper by Dybjer (http://www.cse.chalmers.se/~peterd/papers/Inductive_Families.pdf). However, because the function spaces are so huge, types like Ord require really large ordinals to interpret.