Under dependent choice, algebras for a finitary monad on a complete cocomplete locally small category have coequalizers

In $\mathcal{C}$, form $q_0:B\to Q_0$, the coequalizer of $f,g$, and $p_0:TB\to P_0$, the coequalizer of $Tf,Tg$. Their universal properties induce maps $u_0:P_0\to Q_0$ and $v_0:P_0\to T{Q}_0$ characterized by $u_0{p}_0=q_{0}b$ and $v_0{p}_0=T{q}_0$. Both $p_0$ and $q_0$ are epimorphisms.

The category ${\mathcal{C}}^T$ is complete by [L4] and locally small because its hom-sets are subsets of those of $\mathcal{C}$. The walking parallel-pair category is finite and hence small. For any small limit diagram, the finitely many pointwise limits can be chosen without a choice axiom, so [L5] makes the parallel-pair functor category complete. The constant-diagram functor is continuous because these limits are pointwise.

Suppose $(P_n,Q_n,u_n,v_n,p_n,q_n)$ has been constructed with $u_n{p}_n=q_{n}b$ and $v_n{p}_n=T{q}_n$. Put $P_{n+1}=T{Q}_n$, and choose $u_{n+1}:T{Q}_n\to Q_{n+1}$ as a coequalizer of $T(u_n),{\mu }_{Q_n}T(v_n):T{P}_n\rightrightarrows T{Q}_n$. Define $q_{n,n+1}=u_{n+1}{\eta }_{Q_n}$, $v_{n+1}=T{q}_{n,n+1}$, $p_{n+1}=v_n{p}_n$, and $q_{n+1}=q_{n,n+1}{q}_n$. Naturality of $\eta$ and the monad unit law give $q_{n,n+1}{u}_n=u_{n+1}{\eta }_{Q_n}{u}_n=u_{n+1}{v}_n$. Consequently $u_{n+1}{p}_{n+1}=q_{n+1}b$ and $v_{n+1}{p}_{n+1}=T{q}_{n+1}$.

Let $h:(B,b)\to (C,c)$ be any algebra homomorphism with $hf=hg$. Factor it uniquely as $h=k_0{q}_0$. Precomposing with the epimorphism $p_0$ and using step 1.1 gives $cT(k_0)v_0=k_0{u}_0$.

To justify the countable sequence of choices in step 2.1, encode each finite stage by a set. For a state $x$, let $S(x)$ be all valid successor codes of least possible von Neumann rank; it is a nonempty subset of some $V_{\alpha }$, hence a set. Starting with the code from step 1.1, recursively close under $x\mapsto S(x)$ for finitely many steps and take the union over $\mathbb{N}$. Replacement and union make this closure a set on which the successor relation is entire. Applying [L2] to that set gives one compatible sequence of stages.

Suppose $k_n:Q_n\to C$ satisfies $cT(k_n)v_n=k_n{u}_n$. The algebra law for $c$ shows that $cT(k_n)$ coequalizes $T(u_n)$ and ${\mu }_{Q_n}T(v_n)$, so it factors uniquely through $u_{n+1}$ as a map $k_{n+1}:Q_{n+1}\to C$ with $k_{n+1}{u}_{n+1}=cT(k_n)$. The definitions in step 2.1 then give $k_{n+1}{q}_{n,n+1}=k_n$ and $cT(k_{n+1})v_{n+1}=k_{n+1}{u}_{n+1}$, closing the induction.

Form the sequential colimits $Q_{\omega }={\mathrm{colim}}_n{Q}_n$ and $P_{\omega }={\mathrm{colim}}_n{P}_n$, with injections $q_{n,\omega }$ and $p_{n,\omega }$. The identities $q_{n,n+1}{u}_n=u_{n+1}{v}_n$ make the $u_n$ a map of the two sequential diagrams, hence induce $u_{\omega }:P_{\omega }\to Q_{\omega }$. The compatible $q_n$ induce $q_{\omega }:B\to Q_{\omega }$. The shifted identities $P_{n+1}=T{Q}_n$ and $v_{n+1}=T{q}_{n,n+1}$ identify $P_{\omega }$ with ${\mathrm{colim}}_{n}T{Q}_n$.

The natural-number indexing category is filtered, so finitarity [L1] identifies the colimit in step 4.1 with $T{Q}_{\omega }$. Make this identification, so $P_{\omega }=T{Q}_{\omega }$ and the induced comparison $v_{\omega }:P_{\omega }\to T{Q}_{\omega }$ is the identity. Thus $u_{\omega }:T{Q}_{\omega }\to Q_{\omega }$.

For every $n$, naturality of $\eta$ and the definition of $q_{n,n+1}$ give $u_{\omega }{\eta }_{Q_{\omega }}{q}_{n,\omega }=q_{n,\omega }$. The colimit injections are jointly epimorphic, so $u_{\omega }{\eta }_{Q_{\omega }}=1_{Q_{\omega }}$.

The compatible $k_n$ induce $k:Q_{\omega }\to C$. Passing the equations $k_{n+1}{u}_{n+1}=cT(k_n)$ to the colimit gives $k{u}_{\omega }=cT(k)$, and compatibility at stage zero gives $k{q}_{\omega }=h$.

The successor coequalizer equations are $u_{n+1}T(u_n)=u_{n+1}{\mu }_{Q_n}T(v_n)$. Passing these compatible equations to the filtered colimit gives $u_{\omega }T(u_{\omega })=u_{\omega }{\mu }_{Q_{\omega }}T(v_{\omega })=u_{\omega }{\mu }_{Q_{\omega }}$ because $v_{\omega }=1$ in step 5.1. Together with step 6.1, this makes $(Q_{\omega },u_{\omega })$ a $T$-algebra.

Passing $u_n{p}_n=q_{n}b$ and $v_n{p}_n=T{q}_n$ to the colimit gives $u_{\omega }T{q}_{\omega }=q_{\omega }b$, so $q_{\omega }$ is an algebra homomorphism; it coequalizes $f,g$ because $q_0$ does.

By steps 6.2 and 7.1, $k$ is an algebra homomorphism, and step 6.2 gives $k{q}_{\omega }=h$. Therefore the single algebra fork $q_{\omega }$ is a solution set for the constant-diagram functor $\mathrm{\Delta }:{\mathcal{C}}^T\to ({\mathcal{C}}^T{)}^{\bullet \rightrightarrows \bullet }$ at the given parallel pair: every algebra fork factors through it, without a uniqueness assertion.

Apply [L3] to $\mathrm{\Delta }$ using the singleton solution set from step 9.1 and the complete, locally small, and continuity properties proved in step 1.2. The resulting universal arrow is a left adjoint value for $\mathrm{\Delta }$, hence a coequalizer of $f,g$ in ${\mathcal{C}}^T$. Since the pair was arbitrary, all coequalizers exist.