I'm wondering if someone can give me the intuition behind why strict positivity of inductive data types guarantees strong normalization.
To be clear, I see how having negative occurrences leads to divergence, i.e. by defining:
data X where Intro : (X->X) -> X
we can write a divergent function.
But I'm wondering, how can we prove that strictly positive inductive types don't allow for divergence? i.e. is there some induction measure that lets us construct a proof of strong-normalization (using logical relations or similar)? And where does such a proof break down for negative occurrences? Are there any good references that show strong normalization for a language with inductive types?