# Why should you "never resort to polymorphism when initiality would do"?

In the concluding statement of "universe hierarchies", Conor McBride calls it

[...] that key lesson which I learned from James McKinna: never resort to polymorphism when initiality will do.

How can you recognize when you could use initiality instead of polymorphism, and why should you prefer to use initiality?

Initiality comes with a powerful universal property which allows you to, internally, prove statements about the constructions you perform. If you give me an element of data Nat = Z | S Nat, I can perform induction on it.
Polymorphism on the other hand requires you to appeal to external principles such as parametricity (*) to recover similar reasoning principles. If you give me a function of type (a -> a) -> a -> a, I will know it is bound to be a natural number in disguise but will be powerless to exploit that fact.