It is, of course, not impossible that big categories come with an equality of objects, e.g. if one works relative to a base category Set which is a model of ZFC with sufficiently many Grothendieck universes. A very strong such extension is by the axiom that every set appears as element of some Grothendieck universe. For most purposes 2 or 3 nested Grothendieck universes suffice. This may seem strong but is weaker than some of the large cardinal axioms considered by set theorists. As I understand big categories without equality show up necessarily when one works relative to bases much weaker then Set like elementary toposes or "predicative" versions thereof. The reason is that when fibring the base BB over itself via the fundamental (or codomain) fibration P_BB : BP^2 -> BB this fibration is not split. A possibility is to extend BB to the category Idl(BB) (as done in work on Algebraic Set Theory by Awodey et.al. following an advice of Joyal) which provides a model for an intuitionistic theory of classes. One may describe Idl(BB) as the full subcategory of Sh(BB) (sheaves over BB w.r.t. the finite cover topology) such that equality is definable in the sense of Benabou. Of course, not all split fibrations over BB can be obtained as externalisations of categories internal to Idl(BB). But P_BB is equivalent to such a fibration. Of course, this approach just mimicks the classical set theoretic approach which many people dislike. Type theory was mentioned as a possible alternative because via dependent types one can formulate the structure of a category in a most natural way. But if one works in extensional type theory (i.e. "judgemental" and "propositional" equality identified) there is also no problem with equality. Actually extensional type theory with a cumulative sequence of universes is an attractive alternative for those who dislike a set like approach. The current official version of type theory is intensional type theory with a weak "judgemental" equality and a stronger "propositional" equality. The distinguishing feature of intensional type theory is that type checking is decidable (which is not the case for extensional type theory). Living with two equalities doesn't really make one's life easier but it's a price to be paid for having the nice (and practically most useful) property of decidable type checking. But there is a way of turning this defect into an advantage. This was observed in the mid 90s by Martin Hofmann and myself when we considered the model where types are groupoids and families of types are (split) fibrations of groupoids. Of course, the diagonal on a groupoid will be a fibration if and only if the groupoid is discrete. Therefore, we interpreted the equality on a groupoid A as the fibration corresponding to Hom_A(-,-), i.e. equality as being isomorphic. Thus there are different ways of being equal because there are in general different ways of being isomorphic. (Finding models of type theory where there are different ways of being propositionally equal was our main concern in this paper). We also discussed in this paper (Sect.5.4) that one might add axioms claiming for elements of some universe that being equal is equivalent to being isomorphic. In Sect.5.5 of this paper we sketched how to exploit such an extended type theory for formalizing category theory in such a way that equality of objects is equivalent to them being isomorphic. There are 2 defects of the groupoid model, namely that it is 2-dimensional and that it is strong and not weak. In his PhD Thesis Michael Warren has shown that strict \omega-groupoids do form a model of intensional type theory. In a talk some time ago (2006) I suggested to model intensional type theory in the topos SSet of simplicial sets interpreting types as Kan complexes and families of types as Kan fibrations. Recently, in Nov. 2009 V.Voevodsky gave a talk in Munich on "Homotopical Lambda Calculus" where he presented such a setting as a model for type theory where equality can be understood as being isomorphic. The latter was precisely his motivation for doing it. He said he will write up this work in the near future. Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]