Seven trees in one (Q1901018)

This is a pilot project inside ``objective number theory'', as envisaged and begun by Lawvere and Schanuel. More precisely, if a complex number \(T\) satisfies the equation \(T = T^2 + 1\), then it also satisfies \(T^6 = 1\), and hence \(T^7 = T\). But this particular entailment may not only be seen on the level of numbers, but on the level of sets, meaning that an explicit bijection between sets \(T\) and \(T^2 + 1\) (=cartesian product of \(T\) with itself, with an added new base point) entails an explicit bijection between \(T^7\) and \(T\). An explicit bijection between \(T\) and \(T^2 + 1\) exists for instance when \(T\) is the set of (binary) trees; for, a (binary) tree is either just a root, or splits naturally into a pair of subtrees (by removing the root). The author establishes now a very explicit bijection between the set \(T^7\) of seven-tuples of trees and the set \(T\) of trees itself, and also makes sense to the phrase ``very explicit''; one way to make sense to it is as provability in intuitionistic set theory with an added axiom. -- For the general program of objective number theory, see the contributions by Lawvere and Schanuel in: Category theory, Proc. Int. Conf., Como 1990 [\textit{F. W. Lawvere}, Lect. Notes Math. 1488, 279-281 (1991; Zbl 0745.18002); \textit{S. H. Schanuel}, ibid. 379-385 (1991; Zbl 0748.18005)].