The point about axiomatic foundations is not at all deep, and not special to category theory. You can extend the language of Zermelo Frankel set theory by adding a "choice function" which applied to any set of sets returns a function assigning each of those sets a unique selected member. That is a form of global choice. But then, if you do not want choice in general, but only some limited amount of it you might be able to use some operator more germane to your needs -- e.g. for any ideal in a Boolean ring it selects a larger prime ideal. This is weaker than the whole axiom of choice. You can do the same kind of thing in many ways in categorical foundations -- e.g. an operator which to any diagram in a complete category assigns a selected limit.
The general summary you give is quite right: Once limits are chosen the arrows induced by cones under them are unique. The only subtlety is to keep in mind that a limit for a diagram is not just an object, it is an object plus a cone to the diagram. A product for sets S and T is not just a set SxT but the set plus its projection functions p_1:SxT-->S and p_2:SxT-->T. That is essential to the functoriality since that is how the induced functions to SxT are determined.