You need some source of infinite-ness, otherwise the entire theory can be modelled by finite sets. It can be provided by the natural numbers or W types or induc

You need some source of infinite-ness, otherwise the entire theory can be modelled by finite sets. It can be provided by the natural numbers or W types or inductive types, but the naturals are arguably the most fundamental of the three.