Reference. Seven trees in one [blass1995seven]

Following a remark of Lawvere, we explicitly exhibit a particularly elementary bijection between the set $T$ of finite binary trees and the set $T^7$ of seven-tuples of such trees. “Particularly elementary” means that the application of the bijection to a seven-tuple of trees involves case distinctions only down to a fixed depth (namely four) in the given seven-tuple. We clarify how this and similar bijections are related to the free commutative semiring on one generator X subject to $X=1+X^2$. Finally, our main theorem is that the existence of particularly elementary bijections can be deduced from the provable existence, in intuitionistic type theory, of any bijections at all.

@article{blass1995seven,
  title={Seven trees in one},
  author={Blass, Andreas},
  journal={Journal of Pure and Applied Algebra},
  volume={103},
  number={1},
  pages={1--21},
  year={1995},
  publisher={Elsevier}
}