Game semantics for the constructive $\mu$-calculus

We define game semantics for the constructive $\mu$-calculus and prove its equivalence to bi-relational semantics. As an application, we use the game semantics to prove that the $\mu$-calculus collapses to modal logic over the modal logic $\mathsf{IS5}$. We then show the completeness of $\mathsf{IS5}$ extended with fixed-point operators.