Just to respond to one aspect of this: Joyal wrote:
I am also reluctant to base category theory on type theory because constructive mathematics tends to be much more complicated than ordinary mathematics.
I can't speak for others, but I did not intend, in making the suggestion to base category theory without equality for objects on type theory, that constructive mathematics be necessarily also adopted. While many of the adherents of type theory have a constructive point of view, and type theory is a natural home for constructive mathematics, type theory with classical logic is also a perfectly well-defined notion. Its type-theoretic properties are not as good as those of the constructive version, but that's irrelevant for the purposes I had in mind: it can be used as a language just like the ordinary classical first-order logic in which classical set theories such as ZFC are formulated. Mike [For admin and other information see: http://www.mta.ca/~cat-dist/ ]