Let $C$ be a category with pullbacks. Recall that a colimit in $C$ is van Kampen if it is preserved by $C/(-): C^{op} \to CAT$, $c \mapsto C/c$.

We can $C$-internalize everything in sight:

Let $\underline C$ be the $C$-indexed category whose fiber over $c$ is $C/c$; let $\underline C^{op}$ be the $C$-indexed category whose fiber over $c$ is $(C/c)^{op}$. Reindexing is given by pullback in $C$.

Let $\underline{CAT}(C)$ be the $C$-indexed category whose fiber over $c$ is the category of categories fibered over $C/c$, with reindexing by pullback.

Define a $C$-indexed functor $\underline C/(-): \underline C^{op} \to \underline{CAT}(C)$ (on fibers, this maps $(C/c)^{op} \to CAT(C/c)$) as follows. The fiber of $\underline{C}/(d \to c)$ over $e \to c$ is $C/d \times_c e$.

Now let's say that a $C$-internal colimit in $\underline C$ is *internally van Kampen* if it is preserved by $\underline C /(-)$. Say that $C$ *has internally van Kampen colimtis* if all $C$-colimits in $\underline C$ are internally van Kampen.

**Questions:**

Has the notion of "internal van Kampen colimits" been studied before?

Which categories have internally van Kampen colimits? Do they include all locally cartesian closed categories?

**Motivation:**
$\infty$-categorically, a Grothendieck $\infty$-topos is precisely a locally cartesian closed locally presentable $\infty$-category where all colimits are van Kampen. It would be nice to know which $\infty$-categories are "internally topos-like", and the ordinary case seems like a good starting place.

allcolimits can be asked to be van Kampen in the 1-categorical case, only 1-Giraud ones like coproducts, pushouts of monomorphisms, and coequalizers of equivalence relations. If you make this restriction, then presumably one could reproduce the usual proof that Set has ordinary van Kampen colimits to prove in the 'internal language' of any 1-topos that it has internally van Kampen colimits. $\endgroup$ – Mike Shulman Jun 20 '18 at 9:44