 A rejoinder should be added, however. McLarty’s and Awodey’s claim that all mathematical properties expressible in categorical set theory are isomorphism invariant has been contested, e.g., in Tsementzis (2017). In fact, Tsementzis argues that neither ZFC nor ETCS provide fully structuralist foundations for mathematics, since their respective languages do not, after all, exclusively allow for the formulation of invariant properties. Then again, both Makkai’s FOLDS system (Makkai 1995, Other Internet Resources, 1998) and the Univalent Foundations program developed in Homotopy Type Theory (Univalent Foundations Program 2013) seem to meet this condition. Here we have reached another ongoing debate in the literature.