> That is, have an axiom that states that an infinte set exists. Type theories do have that axiom. It takes the form of the axiom that postulates the existence

> That is, have an axiom that states that an infinte set exists. Type theories do have that axiom. It takes the form of the axiom that postulates the existence of inductive types of the kind you've shown.