On Fri, Dec 8, 2017 at 5:15 PM, Vaughan Pratt <pratt@cs.stanford.edu> 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/ ]