There’s a famous dubious argument that “proves” the set of $\mathrm{Tree}$ of (planar, rooted) binary trees is in bijection with the set of $7$-tuples of trees $\mathrm{Tree}^6$.

The argument goes as follows. A binary tree is either empty or a non-empty tree with two children which are binary trees. Thus we have an isomorphism $\mathrm{Tree} \cong 1 + \mathrm{Tree}^2$. Pretending that $\mathrm{Tree}$ is a complex number and using the quadratic formula we obtain

This is of course all a bit silly but as Fiore and Leinster showed, there is a general principle which provides legitimate proofs for arguments such as these. Specifically they prove the following. Let $p, q_1$ and $q_2$ be polynomials over $\mathbb{N}$ (with some conditions on the polynomials which I won’t mention). Suppose that $z = p(z)$ implies $q_1(z) = q_2(z)$ for all $z \in \mathbb{C}$. Then $z = p(z)$ implies $q_1(z) = q_2(z)$ in all categories with a product, coproduct, and terminal object.

This theorem is strong enough to get us our bijection $\mathrm{Tree}^7 \cong \mathrm{Tree}$, but apparently not to fix all nonsense arguments. Consider the following. Let $t$ be the type defined by

type t =
  | A0
  | A1 of t
  | A2 of t * t

(or in other words $t$ is the smallest set satisfying $t = 1 + t + t^2$ or $t$ is the initial algebra for the functor $X \mapsto 1 + X + X^2$ or…).

Then if we imagine $t$ is a complex number, we have $0 = 1 + t^2$ so that $t = \pm i$. Let’s just pick $t = i$ for convenience since the two are indistinguishable. Then just by calculation, we have $\frac{2}{1 - t} = 1 + t$.

Now let’s interpret this equation in terms of types. By another dubious argument, $\frac{1}{1 - t} = 1 + t + t^2 + \dots = \mathrm{List}(t)$ since

Our dubiously obtained equation tells us we should have a bijection $2 \times \mathrm{List}(t) \cong 1 + t$ where $2$ is a type with $2$ elements. There is in fact a very nice such bijection (or really, a family of such bijections indexed by the set of infinite binary strings) described below. I believe the existence of such a thing is not provided by Fiore and Leinster’s theorem. Where does it come from?

Spoiler: The bijection

Let $X_n$ for $n \geq 0$ be the set of elements of $t$ which are of the form and $Y_n$ for $n \geq 1$ those of the form and $Y_0 = { * }$ where $*$ is some fresh guy not in $t$.

Note that for $n > 0$, $X_n \cong Y_n \cong t^n$ by the obvious map which makes a list of all the dangling children $s_i$. It is clear that $X_n$ and $Y_n$ are disjoint and with a bit more thought that $1 + t \cong {*} \sqcup t = \bigsqcup_{n = 0}^\infty (X_n \sqcup Y_n)$ so that