The category \(\int_{\An}C\) admits anima-indexed colimits, and the functor \(\pi\colon \int_{\An}C \to \An\) preserves anima-indexed colimits.
Proof
Consider a functor \(F = (A_{\bullet},X_{\bullet})\colon I \to \int_{\An} C\) for which we wish to construct a colimit, where \(I\) is an anima. Consider the colimit \(A := \colim_{i \in I} A_i\) of the underlying animae, thus extending \(A_{\bullet}\) to a colimit cocone \(\overline{A}_{\bullet}\colon I^{\triangleright} \to \An\). Denote by \(f_i\colon A_i \to A\) the maps in the colimit cocone. The diagram \(F\) is a lift of \(A_{\bullet}\colon I \to \An\), corresponding to a section of the cartesian fibration \(I \times_{\An} \int_{\An} C \to I\). Since \(I\) is an anima, this section is automatically a cartesian section, and it thus defines an object of the category
\[\Gamma_I^{\mathrm{cart}}(I \times_{\An} \int_{\An} C \to I) \quad \simeq \quad \lim_{i \in I\catop} \Fun(A_i, C) \quad \simeq \quad \Fun(\colim_i A_i, C) \quad \simeq \quad \Fun(A,C).\]
This defines an object \(X \in \Fun(A,C)\), hence an object \((A,X) \in \int_{\An}C\). Applying a similar reasoning to the diagram \(\overline{A}_{\bullet}\colon I^{\triangleright} \to \An\), we see that
so that the object \(X\) gives rise to a cartesian section \((\overline{A}_{\bullet},\overline{X}_{\bullet})\colon I^{\triangleright} \to \int_{\An}C\) lifting \(\overline{A}_{\bullet}\), which essentially by construction extends \(X_{\bullet}\). We will show that this is a colimit cocone in \(\int_{\An}C\), which simultaneously establishes both claims of the lemma.To this end, consider another object \((B,Y) \in \int_{\An}C\). We need to show that top map in the following commutative diagram is an equivalence: The bottom map in this diagram is an equivalence by definition of \(A\) as a colimit. Therefore, it suffices to check that the square induces equivalences on vertical fibers over every map of animae \(f\colon A \to B\). Letting \(f_i \colon A_i \to A \xrightarrow{f} B\) denote the composite maps for all \(i\), this map on fibers takes the following form:
But this map is an isomorphism, since the pullback functors along the maps \(A_i \to A\) induce an equivalence \(\Fun(A,C) \iso \lim_{i \in I\catop} \Fun(A_i,C)\), and the restriction of \(X\) to \(A_i\) is \(X_i\) by construction. This finishes the proof.
