proposition: Lemma composedrelativelaxcommutator_unit: relativelaxcommutator_unit composedrelativelaxcommutator_data.
proof: Proof. red; unfold composedrelativelaxcommutator_data; cbn. rewrite (relativelaxcommutator_ldunit γ1). rewrite (relativelaxcommutator_ldunit γ2). etrans. { do 3 apply cancel_postcomposition. apply maponpaths. etrans. { apply (functor_comp (rightwhiskering_functor Mon_V v2)). } do 2 rewrite functor_comp. cbn. apply idpath. } etrans. { apply cancel_postcomposition. repeat rewrite assoc'. do 6 apply maponpaths. etrans. { apply (functor_comp (leftwhiskering_functor Mon_V v1)). } do 2 rewrite functor_comp. cbn. apply idpath. } etrans. { repeat rewrite assoc. do 9 apply cancel_postcomposition. apply pathsinv0, monoidal_associatorinvnatright. } repeat rewrite assoc'. apply maponpaths. etrans. { repeat rewrite assoc. do 8 apply cancel_postcomposition. rewrite <- monoidal_triangleidentity'. rewrite assoc. apply cancel_postcomposition. apply (pr2 (monoidal_associatorisolaw Mon_V _ _ _)). } rewrite id_left. repeat rewrite assoc'. apply maponpaths. etrans. { do 6 apply maponpaths. apply monoidal_associatorinvnatleft. } repeat rewrite assoc. apply cancel_postcomposition. etrans. { do 4 apply cancel_postcomposition. rewrite assoc'. apply maponpaths. apply pathsinv0, monoidal_associatornatleftright. } etrans. { do 3 apply cancel_postcomposition. repeat rewrite assoc'. do 2 apply maponpaths. etrans. { apply pathsinv0, (functor_comp (leftwhiskering_functor Mon_V v1)). } apply maponpaths. etrans. { apply pathsinv0, (functor_comp (rightwhiskering_functor Mon_V v2)). } apply (functor_id_id _ _ (rightwhiskering_functor Mon_V v2)). apply (pr2 (fmonoidal_preservesunitstrongly U)). } rewrite functor_id. rewrite id_right. etrans. { repeat rewrite assoc'. do 3 apply maponpaths. apply monoidal_triangle_identity''_inv. } etrans. { apply maponpaths. rewrite assoc. apply cancel_postcomposition. apply monoidal_triangleidentity. } rewrite assoc. etrans. { apply cancel_postcomposition. etrans. { apply pathsinv0, (functor_comp (rightwhiskering_functor Mon_V v2)). } apply (functor_id_id _ _ (rightwhiskering_functor Mon_V v2)). apply (monoidal_rightunitorisolaw Mon_V). } apply id_left. 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.PrecategoryBinProduct UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Functors UniMath.CategoryTheory.Actegories.Actegories UniMath.CategoryTheory.Actegories.MorphismsOfActegories UniMath.CategoryTheory.Actegories.ConstructionOfActegories UniMath.CategoryTheory.coslicecat UniMath.CategoryTheory.Monoidal.Examples.MonoidalPointedObjects UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Actegories.CoproductsInActegories UniMath.CategoryTheory.Actegories.ProductsInActegories UniMath.CategoryTheory.Actegories.ProductActegory