proposition: Lemma lax_lineators_for_actegory_from_precomp_CAT_and_self_action_agree (F : functor [C, C] [C, C]) : lineator_lax (Mon_endo C) (actegory_from_precomp_CAT C C) (actegory_from_precomp_CAT C C) F = lineator_lax (Mon_endo C) (actegory_with_canonical_self_action (Mon_endo C)) (actegory_with_canonical_self_action (Mon_endo C)) F.
proof: Proof. apply idpath. Qed.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.BicatOfCatsElementary UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Examples.EndofunctorsMonoidalElementary UniMath.CategoryTheory.Actegories.Actegories UniMath.CategoryTheory.Actegories.ConstructionOfActegories UniMath.CategoryTheory.Actegories.MorphismsOfActegories UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Actegories.CoproductsInActegories