As to articulating a way to avoid ever using identity of objects and identity of categories, John Baez writes
I think Michael Makkai has done it. He has formulated a foundational approach to mathematics based on infinity-categories, in which equality plays no fundamental role:
http://www.math.mcgill.ca/makkai/mltomcat04/mltomcat04.pdf
I think some approach along these general lines might ultimately become quite popular.
But so far as know, this remains an approach, and not any specific set of axioms offered as foundation. In this paper Michael defines "multitopic ω-category" more or less analogously to how Eilenberg and Mac~Lane defined "category," and he defines "the (large) multitopic set of all (small) multitopic ω-categories" using that definition. If I understand these correctly (and have not, for example, confused intuitive motivation with strict definition) they take for granted such as ideas as the category Set of sets, and Set-valued functors. While Eilenberg and Mac~Lane saw (and referred to) the foundational significance of their ideas, they did not offer their definition as a foundation per se. And they were right. Lawvere's foundations ETCS and CCAF are first-order axiomatizations which suffice to prove the theorems of mathematics (exactly which theorems depending on exactly which axioms, but he clearly defined variants suited to classical analysis and various extensions of that). Has anyone yet offered a first-order (or ML-typetheoretic) axiomatization of mathematics along Makkai's lines? Popular is another question! And I am not worried about finding a final form of such axioms. But I do not yet know of such axioms. best, Colin [For admin and other information see: http://www.mta.ca/~cat-dist/ ]