Lemma composedrelativelaxcommutator_unit: relativelaxcommutator_unit composedrelativelaxcommutator_data. 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.
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.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.whiskering. 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.Actegories.ConstructionOfActegories. Require Import UniMath.CategoryTheory.coslicecat. Require Import UniMath.CategoryTheory.Monoidal.Examples.MonoidalPointedObjects. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Actegories.CoproductsInActegories. Require Import UniMath.CategoryTheory.Actegories.ProductsInActegories. Require Import UniMath.CategoryTheory.Actegories.ProductActegory. Import BifunctorNotations. Import MonoidalNotations. Import ActegoryNotations. Section ActegoryMorphismFromRelativeLaxCommutator. End ActegoryMorphismFromRelativeLaxCommutator.