Existence of a construction in Universal Algebra: infinite trees

Is anything known about the following construction? Fix a signature (function symbols with arities incl 0) Sigma and a Sigma-algebra A. Construct a new Sigma-algebra T(A) as follows: The carrier set of T(A) comprises possibly infinite trees whose nodes are labelled with function symbols in such a way that a node labelled with a k-ary function symbol has exactly k children. Thus, in particular, a leaf must be labelled with a constant symbol and if Sigma has no constant symbols then there will only be infinite trees. The carrier set T(A) is now understood modulo the largest equivalence relation ~ such that if t~t' then one can write t = u(t1,...tl) and t'=u'(t1',...,tl') for terms over Sigma in the standard sense u, u' with variables x1..xl and trees t1,...,tl,t1',...,tl'. Moreover, u=u' must hold in A and t1~t1', ..., tl~tl'. Of course, the witnessing terms u and u' should not just be x1, but rather something starting beginning with a proper function symbol.

-
In the case of multi-unary types, this seems to be (one-sided) infinite words, and the equivalence relation is trivial if I understand it correctly. Can you say more about why and what else you expect from the equivalence relation? –  The Masked Avenger Feb 26 '14 at 7:37
Eg if the algebra A is the natural numbers with 0,1,+,* then, for example the trees +(t1,t2) and +(t2,t1) would be identified (no matter what t1, t2 are) because the terms x+y or +(x,y) and y+x are equal in that algebra. A similar thing is possible when you only have unary function symbols, e.g. A is the natural numbers with the mod2 operation. Then mod2(mod2(t)) = mod2(t) no matter what t is. –  Martin Hofmann Feb 26 '14 at 7:53
So by u=u' must hold in A, does this mean an identity of A in which u and u' are derived operations and not necessarily basic operations of the type? Most of what I am aware of does not use this construction explicitly, assuming it is well defined. I imagine it would have some use in symbolic dynamics. I look forward to other responses to the question. Also, I suspect T(A) or a suitable analog will turn out to be a filtered limit of free algebras from the variety generated by A. –  The Masked Avenger Feb 26 '14 at 8:06
An issue that I see is that the equivalence relation on such trees is not "nicely" generated as congruences are on a term algebra. The example in mind is an infinite binary tree in a type with two binary operations, with the red one being commutative. One wants a tree with red leftmost branch equivalent to a tree with red rightmost branch. One gets this in the case of term algebras; how would it work for an infinite tree? –  The Masked Avenger Feb 26 '14 at 19:17
Thank you, the suggestion with filtered limits could be helpful. Re the second question (red/black) note that equivalence is defined as a greatest fixpoint. To show that t and t' are equivalent it suffices to exhibit an equivalence relation that identifies t and t' and satisfies the compatibility property mentioned in my original post. –  Martin Hofmann Feb 27 '14 at 9:32