Every type-to-type function defined by a regular term is regular under string representation (Theorem C.5.4 of Transducers, the implication from terms to regular functions). The proof is an induction on the term: every atomic term is computed, on representations, by a rational or a regular string-to-string function — reading a representation with a bracket counter capped at the height of the type — and the four combinators preserve regularity under representation, composition by Theorem C.1.1, pairing and co-pairing through the closure properties of Lemma C.2.10, and map through map lifting.