proposition: Lemma Mon_alg_action_alg_map_rel {T : pointed} (X : Mon_alg T) (A : C) : luinv^{ V }_{ pr1 X ⊗_{ V} A} · pointed_pt T ⊗^{ V}_{r} (pr1 X ⊗_{ V} A) · (αinv^{ V }_{ T, pr1 X, A} · pr12 X ⊗^{ V}_{r} A) = identity _.
proof: Proof. destruct X as [X [x xrel]]. set (trinv := monoidal_triangle_identity'_inv V X A). set (associnvnat := monoidal_associatorinvnatright V _ _ X A (pointed_pt T)). set (whiskerrightcomp := bifunctor_rightcomp V). etrans. apply assoc. etrans. apply assoc4. etrans. apply maponpaths_2. apply maponpaths. exact associnvnat. etrans. apply cancel_postcomposition. apply assoc. etrans. do 2 apply cancel_postcomposition. exact trinv. etrans. apply cancel_postcomposition. exact (pathsinv0 (whiskerrightcomp A _ _ _ _ _)). etrans. exact (pathsinv0 (whiskerrightcomp A _ _ _ _ _)). etrans. apply maponpaths. exact xrel. apply (bifunctor_rightid V). Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.NaturalTransformations UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.CategoriesOfMonoids