proposition: Lemma Tinf_mul_alg_map_commutes : (Mon_alg_map _ (pr2 TinfM)) ⊗^{ V}_{r} Tinf · Tinf_monoid_mul = α^{V}_{_, _, _} · T ⊗^{ V}_{l} Tinf_monoid_mul · (Mon_alg_map _ (pr2 TinfM)).
proof: Proof. apply (pre_comp_with_z_iso_is_inj (is_inverse_in_precat_inv (monoidal_associatorisolaw V _ _ _))). apply pathsinv0. etrans. apply assoc. etrans. apply cancel_postcomposition, assoc. etrans. apply cancel_postcomposition. etrans. apply cancel_postcomposition. apply (monoidal_associatorisolaw V). apply id_left. set (ccTinf := free_monoid_coeq_sequence_colim_on I_{V}). set (rt_ccTinf := rt_chain Tinf _ _ _ (isColimCocone_from_ColimCocone ccTinf)). set (rt_colim := free_monoid_coeq_sequence_rightwhisker_colim_on Tinf I_{V}). set (iso := (_,, isColim_is_z_iso _ rt_colim _ _ rt_ccTinf) : z_iso _ _). set (Tiso := (_,, is_z_iso_leftwhiskering_z_iso V T _ (pr2 iso)) : z_iso _ _). apply (pre_comp_with_z_iso_is_inj Tiso). set (rtiso := rt_chain_colim_iso Tinf). set (Trtiso := (_,, is_z_iso_leftwhiskering_z_iso V T _ (pr2 rtiso)) : z_iso _ _). apply (pre_comp_with_z_iso_is_inj (z_iso_inv Trtiso)). set (Vmon := (_,, V) : monoidal_cat). set (isHCC := HT _ (pr2 (free_monoid_coeq_sequence_colim_on Tinf))). set (ltisiso := isColim_is_z_iso _ (CL (mapdiagram (monoidal_left_tensor (pr1 T : Vmon)) (free_monoid_coeq_sequence_diagram_on Tinf))) _ _ isHCC). set (ltiso := (_,, ltisiso) : z_iso _ _). use (pre_comp_with_z_iso_is_inj ltiso). use colimArrowUnique'. intro v. etrans. apply assoc. etrans. apply cancel_postcomposition. apply (colimArrowCommutes). etrans. apply assoc. etrans. apply cancel_postcomposition. { etrans. apply assoc'. etrans. apply cancel_postcomposition. apply (bifunctor_rightid V). etrans. apply id_left. etrans. exact (pathsinv0 (bifunctor_leftcomp V _ _ _ _ _ _)). etrans. apply maponpaths. apply (colimOfArrowsIn). apply (bifunctor_leftcomp V). } etrans. apply assoc'. etrans. apply cancel_precomposition. { etrans. apply assoc. etrans. apply cancel_postcomposition. etrans. exact (pathsinv0 (bifunctor_leftcomp V _ _ _ _ _ _)). apply maponpaths. apply (colimArrowCommutes). etrans. apply assoc. etrans. apply cancel_postcomposition. etrans. exact (pathsinv0 (bifunctor_leftcomp V _ _ _ _ _ _)). apply maponpaths. etrans. apply cancel_postcomposition. etrans. apply cancel_precomposition. apply (bifunctor_leftid V). apply id_right. etrans. apply assoc. apply cancel_postcomposition. exact (Tinf_monoid_mul_iso_precomp_with_colimIn v). reflexivity. } apply pathsinv0. etrans. apply assoc. etrans. apply cancel_postcomposition. apply (colimArrowCommutes). etrans. apply assoc. etrans. apply cancel_postcomposition. { etrans. apply assoc'. etrans. apply cancel_postcomposition. apply (bifunctor_rightid V). etrans. apply id_left. etrans. exact (pathsinv0 (bifunctor_leftcomp V _ _ _ _ _ _)). etrans. apply maponpaths. apply (colimOfArrowsIn). apply (bifunctor_leftcomp V). } etrans. apply assoc'. apply cancel_precomposition. apply pathsinv0. etrans. apply cancel_postcomposition. apply maponpaths. apply (colimArrowCommutes (free_monoid_coeq_sequence_rightwhisker_colim_on Tinf I_{ V})). etrans. { etrans. exact (pathsinv0 (id_left _)). etrans. apply cancel_postcomposition. exact (pathsinv0 (pr2 (monoidal_associatorisolaw V _ _ _))). etrans. apply assoc'. apply cancel_precomposition. etrans. apply assoc. exact (pathsinv0 (pr22 (free_monoid_coeq_sequence_on_Tinf_pd_Tinf_map v))). } etrans. apply assoc. apply pathsinv0. etrans. { etrans. apply assoc. etrans. apply cancel_postcomposition. etrans. exact (pathsinv0 (bifunctor_leftcomp V _ _ _ _ _ _)). apply maponpaths. apply (colimArrowCommutes). etrans. apply assoc. etrans. apply cancel_postcomposition, cancel_postcomposition. { apply maponpaths. etrans. apply cancel_precomposition. apply (bifunctor_leftid V). apply id_right. } etrans. apply cancel_postcomposition. apply (monoidal_associatorinvnatleftright V). etrans. apply assoc'. apply cancel_precomposition. etrans. apply assoc. etrans. apply cancel_postcomposition. { etrans. exact (pathsinv0 (bifunctor_rightcomp V _ _ _ _ _ _)). etrans. apply maponpaths. exact (Tinf_colimIn_alg_map_commutes v). apply (bifunctor_rightcomp V). } etrans. apply assoc'. apply cancel_precomposition. etrans. apply assoc. etrans. apply cancel_postcomposition. exact (Tinf_monoid_mul_iso_precomp_with_colimIn (S v)). apply (colimArrowCommutes (free_monoid_coeq_sequence_rightwhisker_colim_on Tinf I_{ V}) _ _ (S v)). } apply pathsinv0. etrans. apply assoc'. reflexivity. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Limits.Graphs.Coequalizers UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Chains.Chains UniMath.Combinatorics.StandardFiniteSets UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.CategoriesOfMonoids UniMath.ModelCategories.Generated.GenericFreeMonoid UniMath.ModelCategories.Generated.MonoidalHelpers UniMath.ModelCategories.Helpers