From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/9472 Path: news.gmane.org!.POSTED!not-for-mail From: Michael Shulman Newsgroups: gmane.science.mathematics.categories Subject: Re: How analogous are categorial and material set theories? Date: Mon, 11 Dec 2017 10:54:00 -0800 Message-ID: References: Reply-To: Michael Shulman NNTP-Posting-Host: blaine.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset="UTF-8" X-Trace: blaine.gmane.org 1513094117 29441 195.159.176.226 (12 Dec 2017 15:55:17 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Tue, 12 Dec 2017 15:55:17 +0000 (UTC) Cc: categories To: Vaughan Pratt Original-X-From: majordomo@mlist.mta.ca Tue Dec 12 16:55:12 2017 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtp2.mta.ca ([198.164.44.40]) by blaine.gmane.org with esmtp (Exim 4.84_2) (envelope-from ) id 1eOmtj-0007Ib-3q for gsmc-categories@m.gmane.org; Tue, 12 Dec 2017 16:55:11 +0100 Original-Received: from mlist.mta.ca ([138.73.1.63]:41597) by smtp2.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1eOmuC-0005Zj-Uc; Tue, 12 Dec 2017 11:55:40 -0400 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1eOmsj-0007Y3-6h for categories-list@mlist.mta.ca; Tue, 12 Dec 2017 11:54:09 -0400 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:9472 Archived-At: On Fri, Dec 8, 2017 at 5:15 PM, Vaughan Pratt wrote: > I'm not sure how one argues that CT has natural transformations > however.?? They seem to enter as part of the metatheory, which as usually > presented seems to be pretty set theoretic in its outlook. How do NT's > look in an HOTT account of CT? I'm not sure what you mean by "metatheory" here. You can define categories, functors, and natural transformations inside HoTT in roughly the same way that you can inside set theory. If you're thinking of a "synthetic" theory of categories analogous to how HoTT is a synthetic theory of (higher) groupoids, then that's not a very well developed idea and there are various competing proposals (I'm most familiar with https://arxiv.org/abs/1705.07442); but in all of them that I know of natural transformations also arise "naturally", generally as a sort of "directed homotopy" using a "directed equality type" analogous to the undirected equality type of ordinary HoTT. > The language of the Big Bang Theory is pretty family-oriented, except > for equality which seems somewhat controversial.?? But I digress. > > Vaughan > > > On 12/07/17 10:49 PM, Steve Vickers wrote: >> >> Dear Patrik, >> >> The theory of categories is a first order theory, so what exactly are you >> denying here? >> >> Steve. >> >>> On 7 Dec 2017, at 18:58, peklund@cs.umu.se wrote: >>> >>> Is Category Theory a Theory? I think not. At least not in a logical >>> sense. >>> [For admin and other information see: http://www.mta.ca/~cat-dist/ ]