Game semantics for the constructive $μ$-calculus

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.