A question: categorical foundations of mathematics need to axiomatize the category of sets, not of arbitrary categories, is this correct? If this is true, I feel like categorical foundations would just give us a "structural" (some would say "non-evil") way to talk about sets, not really a different basic idea.

@Timothy Chow: I'd consider that "pre-mathematical" (or "pre-logical") though. I agree that if, instead, we understand logic as including all of that as well, then yes, its basis is not formal: it's a human activity carried out by pencil and paper, minds (i.e. brain configurations), computers, or whatever. At that point, its foundation is a matter of philosophy: e.g. type/token distinction and stuff like that.

Is $V$ of finite rank?

This old question bumped into my notifications. So I decided to modify it a bit for clarity, since its author had disappeared.

@YemonChoi: you're right, I've been a bit sloppy. I just remembered that if a Banach algebra has an involution that makes it into a C*-algebra, then such involution is unique. I was assuming the morphisms on both sides are just continuous homomorphisms. Perhaps it's a bit tautologous (many things in category theory are tautologous in sense though..). If you know some relevant functional analysis to make my answer more interesting you're welcome to do so. :)