I am just reading about Lawvere's ETCS axioms for set theory, mainly this paper: https://arxiv.org/pdf/1212.6543v1.pdf, where Tom Leinster introduces a simplified form of these axioms. I am wondering how could ordinal sets (and ordinal arithmetic, cardinal sets, cardinal arithmetic, etc.) be formalized within this theory. I mean, I know that you can define ordinals to be the isomorphism class of well-ordered sets, but, how could you give a specific characterization of the ordinals within Set? How can you properly study ordinal arithmetic within this theory?
The aim of this question is if an undergraduate course on Axiomatic Set Theory could be constructed that only relied on ETCS axioms (which I think are more related with the activity of the "working mathematician" than ZFC) and could cover the usual topics on ordinal and cardinal arithmetic and transfinite induction and recursion. That's why, although I know nowadays a lot of mathematicians and logicians prefer to understand sets within Topos Theory and HoTT, I think it would be interesting to formalize all these concepts on a simple axiomatic set theory as ETCS.