proposition: Corollary monad_comp_assoc `(f : z ~> M w) `(g : y ~> M z) `(h : x ~> M y) : f <=< (g <=< h) ≈ (f <=< g) <=< h.
proof: Proof. unfold kleisli_compose; cat. now rewrite comp_assoc. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Functor Category.Theory.Monad