[proofplan] We prove directly that an arbitrary finite diagram $F:J \to \mathcal C$ has a colimit. The construction first forms one coproduct $P$ of all objects appearing in the diagram and one coproduct $Q$ of the domains of all arrows in the diagram. Two morphisms $Q \rightrightarrows P$ encode the source and target compatibility relations imposed by the arrows of $J$; their coequalizer is the desired colimit object. The universal property of the coequalizer is then identified exactly with the universal property of a cocone from $F$. [/proofplan] [step:Build the two coproducts encoding objects and arrows] Let $J$ be a finite category and let $F:J \to \mathcal C$ be a functor. Define $\operatorname{Ob}(J)$ to be the set of objects of $J$, and define $\operatorname{Mor}(J)$ to be the set of morphisms of $J$. Since $J$ is finite, both $\operatorname{Ob}(J)$ and $\operatorname{Mor}(J)$ are finite sets. Define $P \in \mathcal C$ to be the finite coproduct \begin{align*} P := \coprod_{j \in \operatorname{Ob}(J)} F(j), \end{align*} with coproduct injections \begin{align*} i_j : F(j) \to P \end{align*} for each object $j \in \operatorname{Ob}(J)$. Define $Q \in \mathcal C$ to be the finite coproduct \begin{align*} Q := \coprod_{\alpha:j \to k \in \operatorname{Mor}(J)} F(j), \end{align*} where the summand indexed by a morphism $\alpha:j \to k$ is the object $F(j)$. Let \begin{align*} r_\alpha : F(j) \to Q \end{align*} denote the coproduct injection corresponding to the morphism $\alpha:j \to k$. If $\operatorname{Ob}(J)$ or $\operatorname{Mor}(J)$ is empty, these coproducts are interpreted as empty coproducts, which exist by hypothesis. [/step] [step:Define the source and target maps from the arrow coproduct] We define two morphisms \begin{align*} s,t:Q \to P \end{align*} by specifying their composites with each coproduct injection $r_\alpha$. For a morphism $\alpha:j \to k$ in $J$, define \begin{align*} s \circ r_\alpha &:= i_j : F(j) \to P,\\ t \circ r_\alpha &:= i_k \circ F(\alpha) : F(j) \to P. \end{align*} The universal property of the coproduct $Q$ gives unique morphisms $s,t:Q \to P$ with these specified composites. [guided] The object $P$ remembers all objects of the diagram without yet imposing the relations given by the arrows. The object $Q$ records every arrow $\alpha:j \to k$ by taking one copy of the source object $F(j)$ for that arrow. For each arrow $\alpha:j \to k$, there are two ways that an element of the source summand $F(j)$ should land in the eventual colimit. One way is to include it directly into the $j$-summand of $P$, giving \begin{align*} s \circ r_\alpha := i_j : F(j) \to P. \end{align*} The other way is to first move along the diagram morphism $F(\alpha):F(j)\to F(k)$ and then include into the $k$-summand of $P$, giving \begin{align*} t \circ r_\alpha := i_k \circ F(\alpha) : F(j) \to P. \end{align*} Because $Q$ is the coproduct of the objects $F(j)$ indexed by arrows $\alpha:j\to k$, specifying these composites with all injections $r_\alpha$ uniquely determines morphisms \begin{align*} s,t:Q \to P. \end{align*} Thus the parallel pair $s,t$ is precisely the categorical record of the relations \begin{align*} i_j \sim i_k \circ F(\alpha) \end{align*} that a cocone over $F$ must satisfy. [/guided] [/step] [step:Coequalize the arrow relations] Since $\mathcal C$ has coequalizers, let \begin{align*} q:P \to L \end{align*} be a coequalizer of the parallel pair $s,t:Q \rightrightarrows P$. Thus \begin{align*} q \circ s = q \circ t, \end{align*} and for every object $c \in \mathcal C$ and every morphism $u:P \to c$ satisfying $u \circ s = u \circ t$, there exists a unique morphism $\bar u:L \to c$ such that \begin{align*} \bar u \circ q = u. \end{align*} For each object $j \in \operatorname{Ob}(J)$, define \begin{align*} \lambda_j : F(j) \to L \end{align*} by \begin{align*} \lambda_j := q \circ i_j. \end{align*} We verify that $(\lambda_j)_{j \in \operatorname{Ob}(J)}$ is a cocone over $F$. Let $\alpha:j \to k$ be a morphism in $J$. Then \begin{align*} \lambda_k \circ F(\alpha) &= q \circ i_k \circ F(\alpha)\\ &= q \circ t \circ r_\alpha\\ &= q \circ s \circ r_\alpha\\ &= q \circ i_j\\ &= \lambda_j. \end{align*} Hence the family $\lambda_j:F(j)\to L$ is compatible with every morphism of $J$. [/step] [step:Show that every compatible cocone factors uniquely through $L$] Let $c \in \mathcal C$ be an object, and let \begin{align*} \mu_j:F(j) \to c \end{align*} be a cocone over $F$, meaning that for every morphism $\alpha:j \to k$ in $J$, \begin{align*} \mu_k \circ F(\alpha)=\mu_j. \end{align*} By the universal property of the coproduct $P$, there is a unique morphism \begin{align*} u:P \to c \end{align*} such that \begin{align*} u \circ i_j = \mu_j \end{align*} for every $j \in \operatorname{Ob}(J)$. We check that $u$ coequalizes $s$ and $t$. For every morphism $\alpha:j \to k$ in $J$, \begin{align*} u \circ s \circ r_\alpha &= u \circ i_j\\ &= \mu_j\\ &= \mu_k \circ F(\alpha)\\ &= u \circ i_k \circ F(\alpha)\\ &= u \circ t \circ r_\alpha. \end{align*} Since morphisms out of a coproduct are determined by their composites with the coproduct injections $r_\alpha$, this implies \begin{align*} u \circ s = u \circ t. \end{align*} Therefore the coequalizer property of $q:P\to L$ gives a unique morphism \begin{align*} \bar u:L \to c \end{align*} such that \begin{align*} \bar u \circ q = u. \end{align*} For each $j \in \operatorname{Ob}(J)$, \begin{align*} \bar u \circ \lambda_j &= \bar u \circ q \circ i_j\\ &= u \circ i_j\\ &= \mu_j. \end{align*} Thus every cocone from $F$ to $c$ factors through the cocone $\lambda_j:F(j)\to L$. [guided] Now suppose we are given any other cocone from $F$ to an object $c$. This means we have morphisms \begin{align*} \mu_j:F(j)\to c \end{align*} for each object $j\in \operatorname{Ob}(J)$, satisfying the compatibility condition \begin{align*} \mu_k \circ F(\alpha)=\mu_j \end{align*} for every arrow $\alpha:j\to k$. The coproduct $P=\coprod_j F(j)$ packages the family $(\mu_j)$ into a single morphism. By the universal property of $P$, there is a unique morphism \begin{align*} u:P\to c \end{align*} such that \begin{align*} u\circ i_j=\mu_j \end{align*} for every object $j$. To use the coequalizer $q:P\to L$, we must verify that $u$ equalizes the two maps $s,t:Q\rightrightarrows P$. It is enough to check equality after precomposition with each coproduct injection $r_\alpha$, because $Q$ is a coproduct. For an arrow $\alpha:j\to k$, we compute \begin{align*} u \circ s \circ r_\alpha &= u \circ i_j\\ &= \mu_j\\ &= \mu_k \circ F(\alpha)\\ &= u \circ i_k \circ F(\alpha)\\ &= u \circ t \circ r_\alpha. \end{align*} The middle equality is exactly the cocone condition for $\mu$. Hence $u\circ s=u\circ t$. The coequalizer property now applies: since $u:P\to c$ coequalizes $s$ and $t$, there is a unique morphism \begin{align*} \bar u:L\to c \end{align*} such that \begin{align*} \bar u\circ q=u. \end{align*} Finally, because $\lambda_j=q\circ i_j$, this factorization sends the constructed colimit cocone to the original cocone: \begin{align*} \bar u \circ \lambda_j &= \bar u \circ q \circ i_j\\ &= u \circ i_j\\ &= \mu_j. \end{align*} Thus any compatible cocone out of $F$ is induced by a unique morphism out of $L$. [/guided] [/step] [step:Prove uniqueness of the factorization and identify the colimit] It remains to prove uniqueness among morphisms $L\to c$ inducing the cocone $(\mu_j)$. Let $h:L\to c$ be any morphism satisfying \begin{align*} h\circ \lambda_j=\mu_j \end{align*} for every $j\in \operatorname{Ob}(J)$. Then for every $j$, \begin{align*} h\circ q\circ i_j &= h\circ \lambda_j\\ &= \mu_j\\ &= u\circ i_j. \end{align*} Since morphisms out of the coproduct $P$ are determined by their composites with the injections $i_j$, we obtain \begin{align*} h\circ q=u. \end{align*} By uniqueness in the coequalizer property of $q:P\to L$, this forces \begin{align*} h=\bar u. \end{align*} Therefore the cocone $(\lambda_j:F(j)\to L)_{j\in \operatorname{Ob}(J)}$ is universal. Since $J$ and $F:J\to\mathcal C$ were arbitrary finite diagrams, every finite diagram in $\mathcal C$ has a colimit. Hence $\mathcal C$ has all finite colimits. [/step]