proposition: Lemma binprod_functor_lineator_laxlaws: lineator_laxlaws _ _ _ _ binprod_functor_lineator_data.
proof: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Actegories.Actegories UniMath.CategoryTheory.Actegories.MorphismsOfActegories UniMath.CategoryTheory.Actegories.ProductActegory UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.ProductCategory UniMath.CategoryTheory.Limits.BinProducts