There’s a famous dubious argument that “proves” the set of Tree of (planar, rooted) binary trees is in bijection with the set of 7-tuples of trees Tree6.
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 Tree≅1+Tree2. Pretending that Tree is a complex number and using the quadratic formula we obtain Tree=1±3i2=e2πi3
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,q1 and q2 be polynomials over N (with some conditions on the polynomials which I won’t mention). Suppose that z=p(z) implies q1(z)=q2(z) for all z∈C. Then z=p(z) implies q1(z)=q2(z) in all categories with a product, coproduct, and terminal object.
This theorem is strong enough to get us our bijection Tree7≅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+t2 or t is the initial algebra for the functor X↦1+X+X2 or…).
Then if we imagine t is a complex number, we have 0=1+t2 so that t=±i. Let’s just pick t=i for convenience since the two are indistinguishable. Then just by calculation, we have 21−t=1+t.
Now let’s interpret this equation in terms of types. By another dubious argument, 11−t=1+t+t2+⋯=List(t) since 1=(1+t+t2+…)−(t+t2+…)=(1−t)(1+t+t2+…).
Our dubiously obtained equation tells us we should have a bijection 2×List(t)≅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?
Let Xn for n≥0 be the set of elements of t which are of the form
and Yn for n≥1 those of the form
and Y0=∗ where ∗ is some fresh guy not in t.
Note that for n>0, Xn≅Yn≅tn by the obvious map which makes a list of all the dangling children si. It is clear that Xn and Yn are disjoint and with a bit more thought that 1+t≅∗⊔t=⨆∞n=0(Xn⊔Yn) so that 1+t≅∞⨆n=0(tn⊔tn) ≅∞⨆n=02tn ≅2×∞⨆n=0tn ≅2×List(t)