Constructive proof of existence of free algebras for infinitary equational theories
It was proved by Andreas Blass in Words, free algebras, and coequalizers that free infinitary algebras are not constructible neither in topoi nor in ZF. It is easy to see that the existence of free algebras for all theories is equivalent to the existence of initial algebras of all theories.
Even though initial algebras do not exist in "the basic constructive mathematics", there are stronger theories in which they do exist and which still can be called constructive. For example, initial algebras can be constructed in homotopy type theory with recursive higher inductive types (see Lumsdaine, Shulman, Semantics of higher inductive types).
As was already pointed out by Valery Isaev, even in the presence of excluded middle initial algebras for equational theories need not exist. I would like to explain a bit what is needed from a constructive point of view.
Suppose $T = (\Sigma, E)$ is an equational theory where $\Sigma$ is a family $\Sigma = (A_\mathrm{op})_{\mathrm{op} \in I}$ of sets $A_\mathrm{op}$ indexed by a set $I$. We think of the elements of $I$ as the operation symbols, and $A_\mathrm{op}$ as the arity of the operation symbol $\mathrm{op}$. (Normally arities are natural numbers, but since we allow infinitary operations it is better for arities to be general sets.)
A $T$-algebra $C$ is given by a carrier set $|C|$ and, for each $\mathrm{op} \in A$, a map $\mathrm{op}_C : |C|^{A_\mathrm{op}}| \to |C|$, such that the equations $E$ are satisfied.
A natural way of constructing the initial $T$-algebra is as follows:
Construct the set of well-founded trees $W_T$ whose branching types are $\Sigma$, i.e., the initial algebra for the polynomial functor $X \mapsto \Sigma_{\mathrm{op} \in I} X^{A_\mathrm{op}}$. This is also known as a $W$-type.
Quotient $W_T$ by the (interpretations of) equations $E$ to obtain a candidate for the initial algebra.
We cannot get either step for free, but in general the first step is the easier one, as it is well understood what it takes to have $W$-types in a constructive setting.
For the second step to go through, one needs to resolve the question posed by the OP, namely, how do we lift operations from the quotient $W_T/E$ to $W_T$? It looks like we need choice. Indeed, it suffices for all the arities $A_\mathrm{op}$ to satisfy choice (to be choice sets, also called projective objects), but is that necessary? I do not know of any way of avoiding choice if one attempts to construct the initial algebra as a quotient of an inductively defined set.
Homotopy type theory offers an alternative. We avoid stratifying the construction of the initial algebra into an inductive construction followed by a quotient. Instead, we make a purely inductive construction: the initial $T$-algebra is the higher-inductive type $X$ with the following constructors:
- for each $\mathrm{op} \in I$, there is a point constructor $\overline{op} : X^{A_\mathrm{op}} \to X$;
- for each equation $\ell_i(x_1, \ldots, x_n) = r_i(x_1, \ldots, x_n)$ in $E$ there is a path constructor $e_i : \prod (x_1, \ldots, x_n : X)\,.\, \overline{\ell}_i(x_1, \ldots, x_n) =_X \overline{r}_i(x_1, \ldots, x_n)$,
- set-truncation: for all $x, y \in X$ and all paths $p, q : x =_X y$ there is a path $\tau_{p,q} : p =_{x =_X y} q$.
For further reference, look at the HoTT book chapter on the real numbers, where a variant of such a construction is used to present the Cauchy completion of rational numbers in an inductive fashion.