Mac Lane's Comparison Theorem for the Kleisli Construction Formalized in Coq. - Ekici, Burak; Kaliszyk, Cezary (Mathematics in Computer Science, 2020)