<p>I finally came up with a proof under the hypotheses of (and thoroughly using) Adamek's fix-point theorem, I'll post it here as soon as I write it down properly.</p>
<p>Anyway, I found a bit late that this is also Corollary 1 of Theorem 4.2 in <a href="https://doi.org/10.1007/BF01752392" rel="nofollow noreferrer">(Lehmann and Smyth 1981)</a>, where “Theorem 4.2” is the categorical Bekić lemma. It is also what the “double dagger law” means in <a href="https://link.springer.com/book/10.1007/978-3-642-78034-9" rel="nofollow noreferrer">(Bloom and Ésik 1993)</a>. Back to the setting of lattices, the corresponding result is standard and is presented as the “Golden lemma” by <a href="https://www.sciencedirect.com/bookseries/studies-in-logic-and-the-foundations-of-mathematics/vol/146/suppl/C" rel="nofollow noreferrer">(Arnold and Niwiński 2001)</a>. This answers the call for references!</p>

CC BY-SA 4.0
2023-08-07T16:16:25.267Z
2023-08-08T15:41:36.070Z
2023-08-08T15:41:36.070Z
sparusaurata
<p>Given a polynomial functor <span class="math-container">$F$</span>, its initial algebra is denoted by <span class="math-container">$\mu X.F(X)$</span>.
Now, if <span class="math-container">$F$</span> is a 2-variable polynomial functor, <span class="math-container">$Y \mapsto \mu X.F(X,Y)$</span> turns out to be functorial and we can, again, (check some hypotheses and) compute the initial algebra <span class="math-container">$\mu Y. \mu X.F(X,Y)$</span>.</p>
<p><strong>Is it true (with or without additional hypotheses) that <span class="math-container">$\mu Y. \mu X.F(X,Y) \simeq \mu Z.F(Z, Z)$</span>?</strong></p>
<p>For example, if <span class="math-container">$F(X,Y) := 1+X+Y$</span>, it amounts to the equality <span class="math-container">$(x+y)^{\ast} = (x^{\ast} (\varepsilon + y))^{\ast}$</span> on words.</p>
<p>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?</p>
<p>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.</p>

CC BY-SA 4.0
2023-06-14T21:09:56.127Z
Try $F(X, Y) := 1 + X \times Y$.
Andrej Bauer
CC BY-SA 4.0
2023-06-15T08:52:04.520Z
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?
sparusaurata
CC BY-SA 4.0
2023-06-15T21:12:35.790Z
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](https://en.wikipedia.org/wiki/Rose_tree). On the other hand $\mu Z . 1 + Z \times Z$ is the type of unlabeled binary trees.
Andrej Bauer
CC BY-SA 4.0
2023-06-22T12:08:41.027Z
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!
sparusaurata
CC BY-SA 4.0
2023-06-22T12:15:14.227Z
So I still hope I will find a proof under the assumptions of Adamek's theorem (or maybe some stronger ones?), involving commutation of colimits — but I wonder whether there is some literature about it that I didn't find, or some category theory ninja one-liner...
sparusaurata
CC BY-SA 4.0
2023-06-23T20:33:08.187Z
So we come to the point I was waiting for, so that I can ask the question: What do you mean by "isomorphic"? Isomorphic in what category, precisely?
Andrej Bauer
CC BY-SA 4.0
2023-06-26T13:17:21.583Z
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$.
sparusaurata
CC BY-SA 4.0
2023-06-26T15:42:57.813Z
Ok, that makes sense.
Andrej Bauer
<reference-request><ct.category-theory><algebra><fixed-points><inductive-type>
Can the initial algebra of a 2-variable polynomial functor be computed on the diagonal?
sparusaurata
# Can the initial algebra of a 2-variable polynomial functor be computed on the diagonal?

(Asked by: username_0 on 2023-06-14)

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.

**Tags:** reference-request, ct.category-theory, algebra, fixed-points, inductive-type

> **Comments:**
> **username_1**: Try $F(X, Y) := 1 + X \times Y$.  
> **username_0**: 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?  
> **username_1**: 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](https://en.wikipedia.org/wiki/Rose_tree). On the other hand $\mu Z . 1 + Z \times Z$ is the type of unlabeled binary trees.  
> **username_0**: 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!  
> **username_0**: So I still hope I will find a proof under the assumptions of Adamek's theorem (or maybe some stronger ones?), involving commutation of colimits — but I wonder whether there is some literature about it that I didn't find, or some category theory ninja one-liner...  
> **username_1**: So we come to the point I was waiting for, so that I can ask the question: What do you mean by "isomorphic"? Isomorphic in what category, precisely?  
> **username_0**: 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$.  
> **username_1**: Ok, that makes sense.  

---

## 1 answers

### Answer by username_0 on 2023-08-07. Score: 2 | Accepted answer

I finally came up with a proof under the hypotheses of (and thoroughly using) Adamek's fix-point theorem, I'll post it here as soon as I write it down properly.

Anyway, I found a bit late that this is also Corollary 1 of Theorem 4.2 in [(Lehmann and Smyth 1981)](https://doi.org/10.1007/BF01752392), where “Theorem 4.2” is the categorical Bekić lemma. It is also what the “double dagger law” means in [(Bloom and Ésik 1993)](https://link.springer.com/book/10.1007/978-3-642-78034-9). Back to the setting of lattices, the corresponding result is standard and is presented as the “Golden lemma” by [(Arnold and Niwiński 2001)](https://www.sciencedirect.com/bookseries/studies-in-logic-and-the-foundations-of-mathematics/vol/146/suppl/C). This answers the call for references!


---

