Seven Trees in One

• Published in 1994
In the collections
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.

Other information

key
SevenTreesinOne
type
article
2018-11-26
date_published
1994-09-14

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 = {},
}