Dear Eduardo, I agree with many things in your message, but I think you are taking your argument too far. Talking of pullbacks you say:
We precisely teach in category theory courses that you should not work with any particular choice between the choices.
I agree that it is better to avoid such a choice when possible. Yet you cannot define a bicategory of spans without assuming that such a choice has been made; in the same way as you cannot define the (good) monoidal structure of Ab without recurring to a choice of tensor products. Such a situation, we all know, generally arises in non-strict bicategories (and monoidal categories, in particular). Unless you want to redefine bicategories replacing the composition of arrows with an existence property. I still prefer working with a choice (eg of pullbacks) to such a complicated structure. Best regards Marco [For admin and other information see: http://www.mta.ca/~cat-dist/ ]