Re: How analogous are categorial and material set theories?

[Michael Shulman <shulman@sandiego.edu>]

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