@RuneHaugseng I think this slight variant of what @DenisNardin first suggested works: the ∞-category of finite ∞-categories is the smallest subcategory containing Δ⁰ and Δ¹ and closed under colimits indexed by finite ordinary categories.
@OmarAntolín-Camarena Here the rub is what you mean by "finite ordinary categories". In category theory often a category is called finite if it has finitely many objects and finitely many arrows, but that's not necessarily enough for being finite in the ∞-categorical sense! (the standard example is BG for G a finite group)
An idle curiosity: is there a "purely homotopic" way of proving $\pi_iS^1=0$ for $i>1$? The standard proof uses geometry (i.e. covering space theory), but the HoTT folks must have found some way of proving the statement without passing through manifolds (here take $S^1=\Delta^1/\partial \Delta^1$, or if you want a purely homotopic definition, the suspension of $S^0$)
@AlexanderCampbell I guess, I would like it to be as little model dependent as possible
To be clear: I have no objection to proofs using geometry in principle, but I feel that such an elementary homotopy-theoretic fact shouldn't depend on the realization of homotopy types as topological spaces
Perhaps one could prove the equivalence of monoids with categories with one object and then prove that the free monoid on one generator is discrete using the general formula. This feels awfully convoluted, but perhaps it's the best one can do
@DenisNardin Well the proof I had in mind was to argue: (1) that there is an anodyne map $S^1 \to NB\mathbb{Z}$ -- where $NB\mathbb{Z}$ is the nerve of the one-object groupoid suspension of the group $\mathbb{Z}$ -- which has a purely combinatorial proof, and (2) that the nerve $NG$ of any groupoid $G$ has trivial higher homotopy groups, since for $n > 1$ any map $\Delta[n]/\partial\Delta[n] \to NG$ is constant.
But that proof I would definitely describe as model dependent.
Indeed this proves $\Delta^1/\partial \Delta^1\cong B\mathbb{N}$ as an ∞-category and then you can probably cook an argument why group-completing the rhs doesn't produce new homotopy groups
@DenisNardin One way to prove this is by Quillen's Theorem A. (The "lax fibre" of the inclusion $B\mathbb{N} \to B\mathbb{Z}$ is the poset of integers with the usual order, which is weakly contractible.)
@DenisNardin I am aware of that distinction. I was saying that I believe the ∞-category of finite ∞-categories is the smallest subcategory containing Δ⁰ and Δ¹ and closed under colimits indexed by ordinary categories with finitely many objects and finitely many morphisms. That's true, isn't it?
@DenisNardin Oh, sorry! When I was checking in my head I fixated on showing you obtained all finite ∞-categories and forgot to check you don't get more than that.
Yes, after your example of BG I understood why Dylan said posets.
@AlexanderCampbell This argument with Quillen's Theorem A shows that for any commutative monoid M with group completion G, the classifying spaces BM into BG are homotopy equivalent, even if the map from M to G is not injective!
@OmarAntolín-Camarena Right, because group-completion can be realized by a filtered colimit for commutative monoids, and so it preserves discrete objects
Take your time, it wasn't a very complete answer and I am a bit concerned if in the end one didn't have uniqueness of "connection" up to contractible choice.
@DenisNardin How about this disguised version of the covering space proof? Consider two maps $\mathbb{Z} \sqcup \mathbb{Z} \to \mathbb{Z}$: $(id,id)$ and $(id, +1)$. The homotopy pushout is contractible. The maps are $\mathbb{Z}$-equivariant, so you can apply $(-)_{h\mathbb{Z}}$ to the pushout diagram to get that the pushout of $S^0 \to \ast$ with itself is $B \mathbb{Z}$.
(This is like my remark about finite categories in the sense that I haven't carefully thought it through either. :P)
I think you can also run it "backwards", that is, instead of starting with a decomposition of the universal cover, you can compute it. First you build a map $S^1 \to B\mathbb{Z}$ that is an isomorphism on $\pi_1$ (you could use groupoid van Kampen to compute $\pi_1 S^1$). So the suspension pushout square for $S^0$ now lives over $B\mathbb{Z}$, taking homotopy fibres you get the pushout in the previous comment (seeing you get $+1$ on one copy is $\mathbb{Z}$ is the tricky part).
And I think maybe both can be adapted to defining $S^1$ as the homotopy colimit of the loop shaped diagram $pt \circlearrowright$. And I vaguely recall that the "compute the universal cover" method for the loop shaped diagram is actually what is done in HoTT (or at least that's what I thought they were doing when I heard about it).
@DenisNardin I'm a little unsure of the loop-shaped versions of the argument now. I think you'd probably want them to be literally loop shaped, i.e., $\Delta^1/\partial \Delta^1$ (and of course you then need a theory that let's you use that as a diagram shape). But if by loop-shaped diagram you mean something like $B\mathbb{N}$-shaped I think you only prove $B\mathbb{N} \simeq B\mathbb{Z}$, which doesn't really feel $S^1$-y enough.
@OmarAntolín-Camarena Well, what I wanted is "the walking endomorphism", which is of course equivalent to $B\mathbb{N}$ but not obviously so. Literally it is the (homotopy) pushout $\Delta^0\leftarrow \partial \Delta^1\to \Delta^1$
Its groupoid-completion is literally the pushout $\Delta^0\leftarrow \partial\Delta^1\rightarrow \Delta^0$ though, so that argument works. Of course at this point I could get greedy and ask for a proof that the walking endomorphism is a 1-category...
(you can think of any simplicial set as encoding a diagram in Cat_∞, in this way you can talk of many things that look model-dependent in a model-independent way)
Consider $\infty$-categories $A,B,C$. Is it known whether $\underline{\mathrm{Fun}}(A \star B, C) \to \underline{\mathrm{Fun}}(A,C) \times \underline{\mathrm{Fun}}(B,C)$ is a bifibration? I am particularly interested when $A$ or $B$ is equal to $1$.
This is a generalisation of the canonical example of a bifibration $C^{\Delta^1} \to C \times C$ obtained by setting both $A$ and $B$ equal to $1$.
