Lemma binprod_functor_lineator_laxlaws: lineator_laxlaws _ _ _ _ binprod_functor_lineator_data. Proof. red; repeat split. - red. intros v cd1 cd2 g. etrans. { apply precompWithBinProductArrow. } etrans. 2: { apply pathsinv0, postcompWithBinProductArrow. } apply maponpaths_12. + etrans. { apply pathsinv0, (functor_comp (leftwhiskering_functor Act v)). } etrans. 2: { cbn. apply (functor_comp (leftwhiskering_functor Act v)). } apply maponpaths. etrans. { apply BinProductOfArrowsPr1. } apply idpath. + etrans. { apply pathsinv0, (functor_comp (leftwhiskering_functor Act v)). } etrans. 2: { cbn. apply (functor_comp (leftwhiskering_functor Act v)). } apply maponpaths. etrans. { apply BinProductOfArrowsPr2. } apply idpath. - red. intros v1 v2 cd f. etrans. { apply precompWithBinProductArrow. } etrans. 2: { apply pathsinv0, postcompWithBinProductArrow. } apply maponpaths_12. + etrans. { apply (bifunctor_equalwhiskers Act). } apply idpath. + etrans. { apply (bifunctor_equalwhiskers Act). } apply idpath. - red. intros v w cd. etrans. { apply postcompWithBinProductArrow. } etrans. 2: { apply pathsinv0, precompWithBinProductArrow. } apply maponpaths_12. + cbn. etrans. 2: { rewrite assoc'. apply maponpaths. etrans. 2: { apply (functor_comp (leftwhiskering_functor Act v)). } apply maponpaths. apply pathsinv0, BinProductPr1Commutes. } apply pathsinv0, actegory_actornatleft. + cbn. etrans. 2: { rewrite assoc'. apply maponpaths. etrans. 2: { apply (functor_comp (leftwhiskering_functor Act v)). } apply maponpaths. apply pathsinv0, BinProductPr2Commutes. } apply pathsinv0, actegory_actornatleft. - red. intro cd. etrans. { apply postcompWithBinProductArrow. } cbn. etrans. 2: { apply pathsinv0, BinProductArrowEta. } apply maponpaths_12; apply actegory_unitornat. 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.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Actegories.Actegories. Require Import UniMath.CategoryTheory.Actegories.MorphismsOfActegories. Require Import UniMath.CategoryTheory.Actegories.ProductActegory. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.ProductCategory. Require Import UniMath.CategoryTheory.Limits.BinProducts. Import BifunctorNotations.