Modal μ-Calculus for Free in Agda. - Ivan Todorov; Casper Bach Poulsen (TyDe@ICFP, 2024)