# Can the initial algebra of a 2-variable polynomial functor be computed on the diagonal?

Given a polynomial functor $$F$$, its initial algebra is denoted by $$\mu X.F(X)$$. Now, if $$F$$ is a 2-variable polynomial functor, $$Y \mapsto \mu X.F(X,Y)$$ turns out to be functorial and we can, again, (check some hypotheses and) compute the initial algebra $$\mu Y. \mu X.F(X,Y)$$.

Is it true (with or without additional hypotheses) that $$\mu Y. \mu X.F(X,Y) \simeq \mu Z.F(Z, Z)$$?

For example, if $$F(X,Y) := 1+X+Y$$, it amounts to the equality $$(x+y)^{\ast} = (x^{\ast} (\varepsilon + y))^{\ast}$$ on words.

I tried to find a proof using only the initiality of the algebras, but I couldn't — and I suppose it's good news, because if it was true in general, mutual induction wouldn't be of any interest, am I right?

So I guess I have to look at the characterisation of initial algebras by Adamek's theorem, but again I'm not sure what to look for.

• Try $F(X, Y) := 1 + X \times Y$. Jun 14 at 21:09
• Thanks for the hint ! but I'm not sure to understand the counterexample. If I make no mistake, $\mu X.1+X\times Y$ is the set of all $(\dots((\bullet, y),y)\dots)$, ie. sequences of leftmost edges of a binary tree, with right edges pointing to elements of $Y$. Then $\mu Y.\mathrm{this}$ is a description of all binary trees, which are also the elements of $\mu X.1+X\times X$. What I understand is that the difference is the same as the one between BFS and DFS. Where am I wrong? Jun 15 at 8:52
• First, $L(Y) = \mu X . 1 + X \times Y$ are lists of elements of type $Y$, and then $\mu Y . L(Y)$ are unlabeled rose trees. On the other hand $\mu Z . 1 + Z \times Z$ is the type of unlabeled binary trees. Jun 15 at 21:12
• Yes, but these are isomorphic. $L(Y)$, aka lists of type $Y$, are isomorphic to left combs with leaves of type $Y$; then $\mu Y.L(Y)$, aka rose trees, is the type of left combs with leaves of type [left combs with...], which is a description of binary trees. (Similarly, λ-terms can be defined by the alternative "head" signature $M,N ::= x\ |\ \lambda x_1\dots x_m.(M_0)M_1\dots M_n$.) Since we were not 100% confident not to forget something, my colleagues proved the isomorphism in Coq for this $F(X,Y)$: it works! Jun 22 at 12:08
• I guess it's in the category of $F\circ\Delta$-algebras (where $\Delta$ is the diagonal, ie. $F\circ\Delta : X \mapsto F(X,X)$). In practice, I want the isomorphism to be compatible with the signature carried by $F$. Jun 26 at 13:17