  We define game semantics for the constructive $\mu$-calculus and prove its
equivalence to bi-relational semantics. We use the game semantics to prove that
the $\mu$-calculus collapses to modal logic over constructive variants of
$\mathsf{S5}$. Finally, we use the collapse to prove the completeness of
constructive variants of $\mathsf{S5}$ with fixed-point operators.
