proposition: Fact compose_pure_l {A B C D} (f: A -> B) (g: B -> C) (k: Kleisli m C D) : (pure f >>> (pure g >>> k) ⩯ pure (g ∘ f) >>> k)%cat.
proof: Proof. rewrite <- cat_assoc. rewrite compose_pure. reflexivity. Qed.
imports: Coq(Program Setoid Morphisms RelationClasses) ExtLib(Structures.Monad) ITree(Basics.Basics Basics.Category Basics.Monad Basics.CategoryFunctor Basics.CategoryKleisli Basics.Function)