Is it constructively true that all (not necessarily finitary) equational theories $T = (\Sigma, E)$ have an initial model?
The usual proof for finitary equational theories I know constructs first from the signature $\Sigma$ the set $P$ of syntax trees/preterms. This set is by construction the initial model of the theory $(\Sigma, \emptyset)$, i.e. will usually not satisfy equations $E$. One then considers the congruence $R \subseteq P \times P$ generated by (all interpretations of) the equations in $E$, and proves that $Q = P / R$ is a model of $T$ and then that it is the initial one.
If $\Sigma$ contains an operation symbol $f$ of non-finitary arity $A$ then I struggle with defining the operations on the quotient $Q$. The interpretation of $f$ for $Q$ should be a function $f_Q : Q^A \rightarrow Q$, and should be defined in terms of the function $f_P : P^A \rightarrow P$ on syntax trees. If $A$ was finite, then any given map $x : A \rightarrow Q$ could be lifted along $P \twoheadrightarrow Q$ to a map $x' : A \rightarrow P$, and then $f_Q(x)$ could be defined as the residue class of $f_P(x')$ in $Q$. But if $A$ is not a choice object/set, then the proof is stuck here.
Is there a way to get around this issue without assuming choice, or is it maybe known that the existence of certain initial algebras implies some version of the axiom of choice?
EDIT: The reference pointed out by Valery Isaev contains the answer to my questions. There are models of ZF (without C) in which there is no initial algebra for a certain equational theory, in particular it cannot be proved to exist using just constructive logic. On the other hand, initial algebras exist for all theories in all Grothendieck toposes provided that AC holds in the metatheory, so all choice principles that fail to hold in some Grothendieck topos don't follow from the existence of initial algebras.