I am not by any means an expert in category theory. Anyway whenever I have studied a concept in category theory I have always had the feeling that most of the subtleties introduced are artificial.


For a few examples:


-one does not usually consider isomorphic, but rather equivalent categories


-universal objects are unique only up to a canonical isomorphism


-the category of categories is really a 2-category, so some natural constructions do not yield functors into categories, but only pseudofunctors


-cleavages of fibered categories do not always split


....


My question is: can skeleta be used to simplify all this stuff? It looks like building everything using skeleta from the beginning would remove a lot of indeterminacies in these constructions. On the other hand it may be the case that this subtleties are really intrinsic, and so using skeleta, which are not canonically determined, would only move the difficulties around.



Can skeleta simplify category theory?
The first, and perhaps most important, point is that *hardly any categories that occur in nature are skeletal*. The axiom of choice implies that every category is equivalent to a skeletal one, but such a skeleton is usually artifical and non-canonical. Thus, even if using skeletal categories simplified category theory, it would not mean that the *subtleties* were artifical, but rather that the naturally occurring subtleties could be removed by an artificial construction (the skeleton).


In fact, however, skeletons don't actually simplify much of anything in category theory. It is true, for instance, that any functor between skeletal categories which is part of an equivalence of categories is actually an isomorphism of categories. However, this isn't really useful because, as mentioned above, most interesting categories are not skeletal. So in practice, one would either still have to deal either with equivalences of categories, or be constantly replacing categories by equivalent skeletal ones, which is even more tedious (and you'd still need the *notion* of "equivalence" in order to know what it means to replace a category by an "equivalent" skeletal one).


In all the other examples you mention, skeletal categories don't even simplify things that much. In general, not every pseudofunctor between 2-categories is equivalent to a strict functor, and skeletality won't help you here. Even if the hom-categories of your 2-categories are skeletal, there can still be pseudofunctors that aren't equivalent to strict ones, because the *data* of a pseudofunctor includes coherence isomorphisms that may not be identities. Similarly for cloven and split fibrations. A similar question was raised in the query box [here](http://ncatlab.org/nlab/show/Grothendieck+fibration): important data can be encoded in coherence isomorphisms even when they are automorphisms.


The argument in CWM mentioned by Leonid is another good example of the uselessness of skeletons. Here's one final one that's bitten me in the past. You mention that universal objects are unique only up to (unique specified) isomorphism. So one might think that in a *skeletal* category, universal objects would be unique on the nose. This is actually *false*, because a universal object is not just an object, but an object together with data exhibiting its universal property, and a single object can have a given universal property in more than one way.


For instance, a product of objects A and B is an object P *together with* projections P→A and P→B satisfying a universal property. If Q is another object with projections Q→A and Q→B and the same property, then from the universal properties we obtain a unique specified isomorphism P≅Q. Now if the category is skeletal, then we must have P=Q, but *that doesn't mean the isomorphism P≅Q is the identity*. In fact, if P is a product of A and B with the projections P→A and P→B, then composing these two projections with any automorphism of P produces another product of A and B, which happens to have the same vertex object P but has different projections. So assuming that your category is skeletal doesn't actually make anything any more unique.


