Dear André
Many people seem to distrust the equality relation between the objects of a (large) category. Is this a philosophical conundrum or a mathematical problem?
Can we define a notion of (large) category without supposing that its (large) set of objects has a diagonal?
Yes, this is precisely what one does in formalising category theory in an (intensional) dependent type theory. (Mike Shulman has alluded to this in a previous message to this list.) Since in such a type theory one does not have quotients of equivalence relations, one typically works not with raw types but with setoids (=types equipped with an equivalence relation in the internal logic). The category of such setoids is well behaved---at least an LCC pretopos---but the notion of internal category in this pretopos is generally not what one is interested in. Instead one takes a category internal to the type theory to be given by a type of objects O, together with an OxO indexed family of hom-setoids O(x,y), composition and identities which are maps of setoids, and associativity and unitality witnessed by elements of the hom-setoid equality. In this setting, we may not talk of equality of objects (since O is not a setoid but only a type) but may talk of the equality of any pair of parallel arrows. This notion is due to Peter Aczel and there is a fairly extensive development of it in the proof assistant Coq by Gérard Huet and Amokrane Saïbi. Some consequences of the definition are, e.g., that the collection of all small categories does no longer forms a category, but only a bicategory (since one cannot speak of equality of functors, since this would require equality of objects in the codomain). Some work on this has been done by Olov Wilander. Since the category of sets is a model of extensional, and so also intensional, type theory, one may interpret what the above means in this context to obtain, within a classical (or at least impredicative) metatheory, a notion of category meeting your requirements. In fact such non-standard categories may be seen as special kinds of tricategory (in the usual sense). Indeed, in the set-based model of type theory, a setoid is given by a set X; for each pair of elements x,y in X, a further set X(x,y); and arrows of composition X(y,z) x X(x,y)-->X(x,z), inverse X(x,y)-->X(y,x) and identity 1-->X(x,x) subject to no axioms. But this is precisely to give a bigroupoid which is locally chaotic, in the sense that between any two parallel 1-cells, there is a unique 2-cell. [From a constructive perspective, not every such bigroupoid would be "OK". The constructively valid ones would be the cofibrant ones, since these may be inductively generated.] From this it follows without difficulty that a category in the constructive sense is precisely a tricategory (in the sense of Gordon-Power-Street) whose every hom-bicategory is a locally chaotic bigroupoid. The use of these non-standard categories is pertinent with regard to Bill Lawvere's comments on the distinction between presentations and the things (theories) that they present. There is a model structure on the category FPCat of small categories with chosen finite products and strict product-preserving maps whose cofibrant objects are, up to retracts, the (many-sorted) Lawvere theories. One may define, in a similar way, a category FPCat' whose objects are non-standard categories with finite products, and whose morphisms are strict structure-preserving maps: and on this there is a model structure (or at least the cofibration-trivial fibration half of a model structure) whose cofibrant objects are "equational presentations of Lawvere theories": one has not only the sorts, and the generating operations, but also the generating equalities between composite operations. There is an adjunction between FPCat and FPCat' which is the left-hand of the two adjunctions described by Bill. Richard [For admin and other information see: http://www.mta.ca/~cat-dist/ ]