proposition: Lemma η_bind_fun {X Y : sortToC} (f : ∏ t, C⟦pr1 X t,pr1 (M Y) t⟧) (t : sort) : η_fun t · bind_fun f t = f t.
proof: Proof. exact (nat_trans_eq_pointwise (η_bind (sortToC_fun f)) 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