fact: Definition kleisli_compose `(f : a → m b) `(g : b → m c) : a → m c := fun x => (f x >>= g)%category.
imports: Category.Lib Category.Theory.Category Category.Theory.Functor Category.Theory.Monad Category.Instance.Coq