Lemma actegory_binprod_action_data_is_bifunctor : is_bifunctor actegory_binprod_action_data. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Functors. Require Import UniMath.CategoryTheory.Actegories.Actegories. Require Import UniMath.CategoryTheory.Actegories.MorphismsOfActegories. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.ProductCategory. Import BifunctorNotations. Import MonoidalNotations. Import ActegoryNotations.