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