In “Types and Programming Languages”, Pierce gives a translation from recursive types ($ \mu$ types) to types expressed as regular trees: possibly infinite trees, but with finitely many distinct subtrees.
I’m wondering, is the converse true? Can every regular tree type be expressed using the $ \mu$ fixpoint notation? It seems obvious that this can be done if you have mutually recursive types: you have a type for each subtree of the regular tree type. But can it be done with singly recursive types?