Content created by Egbert Rijke and Fredrik Bakke.
Created on 2023-10-22.
Last modified on 2023-11-24.
The universal tree is the coinductive type associated to the polynomial endofunctor
X ↦ Σ 𝒰 (λ T → Xᵀ).
Note that this is the same polynomial endofunctor that we used to define the type of multisets, which is the universal well-founded tree.