From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/9470 Path: news.gmane.org!.POSTED!not-for-mail From: Jacques Carette Newsgroups: gmane.science.mathematics.categories Subject: Re: How analogous are categorial and material set theories? Date: Sun, 10 Dec 2017 13:12:40 -0500 Message-ID: References: Reply-To: Jacques Carette NNTP-Posting-Host: blaine.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset="utf-8"; format=flowed Content-Transfer-Encoding: 7bit X-Trace: blaine.gmane.org 1512932263 10040 195.159.176.226 (10 Dec 2017 18:57:43 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Sun, 10 Dec 2017 18:57:43 +0000 (UTC) To: Vaughan Pratt , Original-X-From: majordomo@mlist.mta.ca Sun Dec 10 19:57:38 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 1eO6nC-0002LV-1w for gsmc-categories@m.gmane.org; Sun, 10 Dec 2017 19:57:38 +0100 Original-Received: from mlist.mta.ca ([138.73.1.63]:41036) by smtp2.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1eO6no-00046i-Pr; Sun, 10 Dec 2017 14:58:16 -0400 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1eO6mL-0006Dg-AH for categories-list@mlist.mta.ca; Sun, 10 Dec 2017 14:56:45 -0400 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:9470 Archived-At: Natural Transformations are homomorphisms of Functors. Working in a dependently-typed setting, this becomes very clear. You don't even need to go to HoTT to see this. By this I mean that if you work 'syntactically', and figure out what it means for a presentation of a theory X to have homomorphisms, then the presentation of Functors qua theory has a natural (ha!) notion of homomorphism, which turns out to be Natural Transformations 'on the nose'. Jacques On 2017-12-08 20:15 , Vaughan Pratt wrote: > I prefer to think of what Steve presumably has in mind here as an > equational theory where composition is 2-ary where 2 is not 1+1 but > rather o--->o. > > One difference between equational logic and first order logic is that > only the former has well-defined homomorphisms (not sure if Gerald Sacks > would have agreed).?? Just as group theory (in Steve's sense) has > homomorphisms, so does category theory in that sense have functors. > > 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? > > 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. >> [For admin and other information see: http://www.mta.ca/~cat-dist/ ]