The n-Category Café

We actually do slightly better than just the automorphism ∞-group. We show the full sub-(∞,1)-category of endofunctors consisting of those endofunctors which happen to be equivalences is equivalent to the discrete group (Z/2)^n.

So any a priori non-invertible natural transformation between these functors is automatically invertible.

But now that I say this it sounds awfully naive.

Yes. The strict globular definition involves saying that lots of things are equal. If you write that down naively in type theory, you’ll end up asserting a lot of paths – but no coherences between them. And if you try to make the coherences precise, then you end up reinventing globular operads.

There are some number of people thinking about this question, including me. It’s tricky even to define an internal $(\infty,1)$-category because it has to involve infinitely much data, and type theory is essentially finitary; you have to encode infinite things by using inductive or coinductive types. I have confidence that we’ll figure it out sooner or later, but I think it will take more work than an “Exercise”. (It’s definitely not clear to me that the answer will end up looking naive and strict; in fact I currently don’t see any way that it can.)

you’ll end up asserting a lot of paths – but no coherences between them.

Maybe I am thinking of a definition that starts out as described in type-theoretic definition of category

Obj : Type

hom (a b : Obj) : Type

but then continues as

triangles : (a b c : Obj) : Type 

components : forall a b c : Obj, triangles a b c -> hom a b * hom b c

composite : forall a b c : Obj, triangles a b c -> hom a c

and asserts coherence maybe along the lines here by saying that the total space map of

components

is an equivalence.

(I am just playing around in a spare minute, this is not meant to be claiming anything.)

That sounds to me like a type-theoretic version of Segal spaces (which one would then presumably want to require to be complete). I would make the triangles dependent on their boundary too:

triangle (a b c : Obj) (f : hom a b) (g : hom b c) (h : hom a c) : Type

and so on, thereby building Reedy fibrancy into the definition. I think that’s one of the most promising avenues; the problem is that it seems to require infinitely many types: Obj, hom, triangle, tetrahedron, etc. We can’t write an infinitely long Coq file. (-:

By the way, I didn’t mean to sound dismissive. It’s important to have lots of people thinking about this. I just wanted to say, I think it’s a hard problem.

It is somewhat rare that Cat/C is cartesian closed. It fails even for C= [2], the free walking composition. Let’s see this explicitly: Recall that [2] is the category with objects 0, 1, and 2 and generated by arrows from 0 to 1, and 1 to 2.

In order for Cat/[2] to be cartesian closed, we need there to be an internal hom, and for that to exist we need for every X in Cat/[2], the fiber product functor

$X \times_{[2]} (-) \; : \; Cat/[2] \rightarrow Cat/[2]$

to commute with colimits. I’ll describe an explicit example where it fails to commute with colimits. Namely we will consider the pushout square which defines [2]. This is a pushout square living over [2] with corners [0], [1], [1], and [2]. These two [1]’s are, respectively, the morphisms from 0 to 1 and 1 to 2 inside [2]. The point [0] maps to the object 1, where the two arrows are glued.

Now we let X = [1], but where the map from X to [2] picks out the composite arrow from 0 to 2. Applying the pullback functor, we see that the above square becomes a square with corners $\emptyset$, [0], [0], and [1]. It is no longer a pushout square.

So the fiber product functor does not commute with colimits, and hence can’t have a right adjoint. There is no internal hom, so Cat/[2] is not cartesian closed.

One might suspect from this that for Cat/C to be cartesian closed we need C to be a category without any compositions. While I think that is sufficient, the story is more complicated. I suspect that Cat/C is cartesian closed whenever C is a groupoid, as long as you are careful to always take homotopy limits and homotopy colimits, and to mean cartesian closed in the correct weak 2-categorical sense.

Of course this doesn’t quite give what you were asking for: a characterization. I wish I understood better precisely which C have Cat/C cartesian closed, but I don’t have good general picture either.

Now that you mention it, it rings a bell. Maybe it skips a generation?

I recall we had a little thread on ‘unicity’ way back when, and I still find myself preferring ‘uniqueness’, but not enough that I feel like revisiting the debate. :-)

I think the whole picture that these guys have come up with is very beautiful—and worth talking some more about, here at a place that takes its name from n-categories.

Wholeheartedly agreed.

It turns out that the 0-truncated $(\infty,n)$-categories are precisely those which contain no nonidentity automorphisms

Just to see if I am missing a subtlety, since you say “it turns out”: this is also obvious, no?

But it’s nice how with the $k$-truncated objects here one gets kind of the “negative” (in the sense of photography) of the $(\infty,k)$-hierarchy. The $k$-truncated $(\infty,n)$-categories have non-trivial invertible morphisms at most up to degree $k$.

The k-connected $(\infty,n)$-categories however still have all $\leq k$-morphism trivial, it seems.

This is how they show that the space of models is $B \mathbb{Z}/2$.

You mean $B (\mathbb{Z}/2)^n$.

Just to see if I am missing a subtlety, since you say “it turns out”: this is also obvious, no?

Well, since I’m not really comfortably conversant with any model of $(\infty,n)$-categories, I’m hesitant to assert that anything about them is “obvious”. But it is very intuitive to me.

You mean $B(\mathbb{Z}/2)^n$.

Thanks; fixed.

I’m hesitant to assert that anything about them is “obvious”.

What I mean is: the $(\infty,1)$-category of $(\infty,n)$-categories – for whatever definition – is defined to be such that the “transfors” all have components in the invertible cells. $k$-Truncation on an object is detected by the vanishing of such invertible $(k+1)$-transfors into it. That’s the case if there no non-trivial invertible $(k+1)$-cells exist.

Of course this is not a formal proof, but I’d think this is easily made a formal proof for any of the existing models. But I admit that I haven’t checked if one runs into subtleties. That’s why I asked.

Well, as I mentioned, it looks like there is a bit of work required to do this starting only from the four axioms. But probably you’re right that in any particular model, it is easy.