Seven Trees in One

• Published in 1994
• Added on 2018-11-26

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.

Links

• http://arxiv.org/abs/math/9405205v1
• http://arxiv.org/pdf/math/9405205v1

Other information

BibTeX entry

@article{SevenTreesinOne,
	key = {SevenTreesinOne},
	type = {article},
	title = {Seven Trees in One},
	author = {Andreas Blass},
	abstract = {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.},
	comment = {},
	date_added = {2018-11-26},
	date_published = {1994-11-11},
	urls = {http://arxiv.org/abs/math/9405205v1,http://arxiv.org/pdf/math/9405205v1},
	collections = {Fun maths facts,Unusual arithmetic},
	url = {http://arxiv.org/abs/math/9405205v1 http://arxiv.org/pdf/math/9405205v1},
	year = 1994,
	urldate = {2018-11-26},
	archivePrefix = {arXiv},
	eprint = {math/9405205},
	primaryClass = {math.LO}
}