On Sat, May 25, 2013 at 5:47 PM, Colin McLarty <colin.mclarty@case.edu> wrote:
This shows we cannot simultaneously maintain:
1) There is a category Set^2 with the usual properties of a functor category. 2) Isomorphic objects are equal in all categories.
I will say some higher category theorists promote another option. They would keep 2, by rejecting 1, by saying there are not functor categories in the standard (1-categorical) sense, but only some infinity-categorical analogue. I do not know if that has ever been systematically spelled out though of course there are projects like Makkai's advocacy of FOLDS that are meant to go that way.
Such an approach has recently been developed here: http://arxiv.org/abs/1303.0584 Univalent categories and the Rezk completion Benedikt Ahrens, Chris Kapulkin, Michael Shulman --- We develop category theory within Univalent Foundations, which is a foundational system for mathematics based on a homotopical interpretation of dependent type theory. In this system, we propose a definition of "category" for which equality and equivalence of categories agree. Such categories satisfy a version of the Univalence Axiom, saying that the type of isomorphisms between any two objects is equivalent to the identity type between these objects; we call them "saturated" or "univalent" categories. Moreover, we show that any category is weakly equivalent to a univalent one in a universal way. In homotopical and higher-categorical semantics, this construction corresponds to a truncated version of the Rezk completion for Segal spaces, and also to the stack completion of a prestack. --- Bas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]