Re: Isbell & MacLane on the insufficiency on skeletal categories

[Bas Spitters <spitters@cs.ru.nl>]

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/ ]