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&lt;Tree&gt;
Tree = (Value, Forest)


Obviously the type above can be reduced to a single type

Tree = (Value, List&lt;Tree&gt;)


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 &amp;= F(A, B)\\
B &amp;= 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 [1] 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 &amp;= \mu_X A . F(A, \mu_X B . G(A,B)), \\
B_0 &amp;= \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$.

[1]: Hans Bekić (1969) Definable operations in general algebras, and the theory of automata and flowcharts. Published posthumously in: Jones C.B. (eds) Programming Languages and Their Definition. (1984) LNCS, vol 177.