There seem to be, broadly speaking, three1 distinct foundations of mathematics: set, type and category theory (the latter as per Lawvere), in which it should be possible to formalize all mathematics except perhaps the theories themselves. For example, I've got a (rather vague) impression that you can formalize all set theory in category theory and vice versa, while you cannot formalize higher inductive types (a foundational tenet of HoTT) in set theory (and I'm not confining type-theoretical foundations of maths to HoTT, it's just an example). So my question is: for all the (three?) foundations, what are their features that cannot be formalized in others? (If you could make a very long list, consider making an overview instead)
EDIT: I understand that the question is difficult, owing to the facts that (1) very few people would be sufficiently knowledgeable to answer it, (2) it's very difficult to prove that something's impossible (and negative existential proofs can be only classical, which undermines their usefulness), and (3) a conjecture is likely to incite an arms race between the theories. Nevertheless, it would be interesting to know what others think
1 @user170039 also mentioned mereology