proposition: Lemma bind_bind_fun {X Y Z : sortToC} (f : ∏ t, C⟦pr1 X t,pr1 (M Y) t⟧) (g : ∏ t, C⟦pr1 Y t, pr1 (M Z) t ⟧) (t : sort) : bind_fun f t · bind_fun g t = bind_fun (λ s, f s · bind_fun g s) t.
proof: Proof. etrans; [apply (nat_trans_eq_pointwise (bind_bind (sortToC_fun f) (sortToC_fun g)) t)|]. apply cancel_postcomposition. assert (H : sortToC_fun f · bind (sortToC_fun g) = sortToC_fun (λ s, f s · bind_fun g s)). { now apply nat_trans_eq; [apply homset_property|]. } exact (nat_trans_eq_pointwise (maponpaths (λ a, # M a) H) t). Qed.
imports: UniMath.Tactics.EnsureStructuredProofs UniMath.Foundations.PartA UniMath.Foundations.PartD UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.Combinatorics.Lists UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.exponentials UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Chains.All UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.Categories.StandardCategories UniMath.CategoryTheory.Groupoids