# Can Isorecursive types capture mutually recursive data types?

I've been reading TAPL, and reached the section on recursive types. I understand the type operator $$\mu$$. For example, the two type expressions are equivalent

NatList = {nil: Unit, cons: (Nat, NatList)}


and $$\mu X. 1 + \text{Nat} \times X$$

I'm confused how I would, using the $$\mu$$ operator, describe mutually recursive types such as

Forest = List<Tree>
Tree = (Value, Forest)


Obviously the type above can be reduced to a single type

Tree = (Value, List<Tree>)


But is there any way to write this using type-theoretic notation? Specifically I am wondering how the isorecursive operations fold and unfold operate on mutually recursive types, since I feel like unfold would have to expand both the definition of Tree and of Forest.

In general, for any type (or domain, or complete lattice) $$X$$ we can consider the least fixed-point operator $$\mu_X : (X \to X) \to X$$. For recursive types we take $$X = \mathsf{Type}$$, i.e., we apply $$\mu$$ at the universe of all types. Given a system of mutually recursive equations \begin{align*} A &= F(A, B)\\ B &= G(A, B) \end{align*} where $$F, G : X \times X \to X$$, rewrite this as a single equation \begin{align*} (A,B) = (F(A,B), G(A,B)) \end{align*} and then define $$H : X \times X \to X \times X$$ by $$H(A,B) = (F(A,B), G(A,B))$$ so that the original system becomes an ordinary fixed point equation $$P = H(P)$$ where $$P = (A, B)$$. This shows that mutual recursion at $$X$$ is ordinary recursion at $$X \times X$$. In terms of the $$\mu$$-operator we may therefore solve the original system as $$(A,B) = \mu_{X \times X} P . (F(P), G(P)).$$ In the case of recursive types, just set $$X = \mathsf{Type}$$.
We may further wonder whether we can replace $$\mu_{X \times X}$$ with two nested applications of $$\mu_X$$, i.e., perhaps it is the case that $$\mu_{X \times X} P . H(P) = \mu_X A . \mu_X B . H(A, B),$$ or something like it. Indeed, Bekić's Lemma  explains how to compute the fixed point on $$X \times X$$ in terms of fixed points on $$X$$, namely $$\mu_{X \times X} (A,B) .(F(A,B), G(A,B)) = (A_0, B_0)$$ where \begin{align*} A_0 &= \mu_X A . F(A, \mu_X B . G(A,B)), \\ B_0 &= \mu_X B . G(A_0,B). \end{align*} Note however that the inner $$\mu_X$$ in $$A_0$$ computes a fixed point in the presence of a free parameter $$A$$, which may be tricky depending on the exact situation.
In summary, you have a choice in solving systems of recursive type equations: either you generalize $$\mu$$ to pairs of types, or you allow parameters to appear when you apply $$\mu$$.