question to Colin about uniqueness in his Replacement axiom

Mike Shulman pointed me out a faulty formulation in my lengthy mail from last Saturday; I take the opportunity of formulating it correctly: In your Replacement axiom (p.48 of your "Philosophia" article) you psotulta the existence of a map f : S -> A such that S_x \cong x^*f for all x : 1->X. Can you prove that this f is unique up to isomorphism, i.e. that wellpointedness for maps entails wellpointedness for families? Thomas