>>792
自然数より型理論が先に生まれたと信じる人がいるとは私には思えないのですが

それでも自然数とは帰納型を用いて定義されるという、後からの整備を否定する理由はないと思います
それに、それらの整備があったからこそVoevodskyなどから発明が生まれて、結果としてLeanの台頭に繋がってますよね