From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/7737 Path: news.gmane.org!not-for-mail From: Bas Spitters Newsgroups: gmane.science.mathematics.categories Subject: Re: Isbell & MacLane on the insufficiency on skeletal categories Date: Sun, 26 May 2013 22:26:11 +0200 Message-ID: References: Reply-To: Bas Spitters NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 X-Trace: ger.gmane.org 1369658125 1513 80.91.229.3 (27 May 2013 12:35:25 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Mon, 27 May 2013 12:35:25 +0000 (UTC) Cc: "categories@mta.ca" To: Colin McLarty Original-X-From: majordomo@mlist.mta.ca Mon May 27 14:35:26 2013 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtp3.mta.ca ([138.73.1.186]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1Ugwe0-0005Xu-Ky for gsmc-categories@m.gmane.org; Mon, 27 May 2013 14:35:20 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:32828) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1Ugwc6-0001mN-QE; Mon, 27 May 2013 09:33:22 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1Ugwc5-00014N-ET for categories-list@mlist.mta.ca; Mon, 27 May 2013 09:33:21 -0300 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:7737 Archived-At: On Sat, May 25, 2013 at 5:47 PM, Colin McLarty 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/ ]