proposition: Lemma actegory_binprod_action_data_is_bifunctor : is_bifunctor actegory_binprod_action_data.
proof: Proof. red; repeat split. * intros v cd. apply dirprodeq. - apply (bifunctor_leftid ActC). - apply (bifunctor_leftid ActD). * intros cd v. apply dirprodeq. - apply (bifunctor_rightid ActC). - apply (bifunctor_rightid ActD). * intros v cd1 cd2 cd3 fg1 fg2. apply dirprodeq. - apply (bifunctor_leftcomp ActC). - apply (bifunctor_leftcomp ActD). * intros cd v1 v2 v3 h1 h2. apply dirprodeq. - apply (bifunctor_rightcomp ActC). - apply (bifunctor_rightcomp ActD). * intros v1 v2 cd1 cd2 h fg. apply dirprodeq. - apply (bifunctor_equalwhiskers ActC). - apply (bifunctor_equalwhiskers ActD). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Functors UniMath.CategoryTheory.Actegories.Actegories UniMath.CategoryTheory.Actegories.MorphismsOfActegories UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.ProductCategory