My impression (which is that of a total non-expert) is the following: Spaces, according to the "homotopy hypothesis," are the same thing as $(\infty, 0)$-categories. This comes out of Lurie's (and Joyal's) work if one accepts that quasi-categories are an appropriate model for $(\infty, 1)$-categories: it's a result that a quasi-category with every 1-morphism invertible is the same thing as a Kan complex. Let $X$ be a space, and let $U, V$ be open subsets which cover $X$. Then we have a homotopy pushout diagram expressing $X$ as the homotopy pushout $U \sqcup_{U \cap V} V$. In other words, if we think in terms of higher *groupoids*, $X$ is the homotopy pushout of the $\infty$-groupoids corresponding to $U, V, U \cap V$. Describing the homotopy type of a homotopy pushout completely (i.e., in terms of homotopy groups and such) is really hard: otherwise we would know all the homotopy groups of spheres! What I take from this is that explicit models for higher category theory that one can easily compute with are likely to be very complicated, or otherwise homotopy theory would become easy. However, there might be more luck if we restrict to special cases. For instance, there is an equivalence between 1-truncated spaces (spaces with no higher homotopy groups than $\pi_1$) and groupoids, given by taking the fundamental groupoid. As it happens, we can compute with groupoids: there is, for instance, a nice model category presentation of groupoids, and we can work out what the homotopy pushout of groupoids is. Since truncation below $n$ is a left adjoint, this then amounts to saying that taking the fundamental groupoid sends homotopy pushout squares in spaces to homotopy pushout squares in groupoids. This is precisely the classical van Kampen theorem (stated for groupoids rather than groups, though.) More generally, we can say that the "fundamental $n$-groupoid of a space" (by which I mean the truncation below $n$) commutes with homotopy push-outs. (Example: if we want to show that $\pi_1(S^1) = \mathbb{Z}$, we observe that $S^1 $ is a homotopy pushout $\ast_{\sqcup S^0} \ast$, so we have to compute the "suspension" of the discrete groupoid on two elements. Taking the homotopy pushout amounts to adding two isomorphisms identifying the two points, which gives a groupoid equivalent to $\mathbb{Z}$.) I understand that you have done work generalizing the classical van Kampen theorem to higher homotopy groups. My guess that, in Lurie's language, some of that would translate into the construction of explicit algebraic model for 2-and-higher-groupoids (as opposed to 2-truncated spaces) and a means of computing homotopy pushouts (but I'm only speculating here), i.e., it seems to me that it would be quite different from what "Higher Algebra" does.