proposition: Fact compose_pure {A B C} (ab : A -> B) (bc : B -> C) : (pure ab >>> pure bc ⩯ pure (ab >>> bc))%cat.
proof: Proof. intros a. unfold pure, cat, Cat_Kleisli. rewrite bind_ret_l. reflexivity. Qed.
imports: Coq(Program Setoid Morphisms RelationClasses) ExtLib(Structures.Monad) ITree(Basics.Basics Basics.Category Basics.Monad Basics.CategoryFunctor Basics.CategoryKleisli Basics.Function)