proposition: Lemma can_colimArrow_forms_cocone (A : C) : forms_cocone (leftwhisker_chain_with T (free_monoid_coeq_sequence_diagram_on A)) (λ n : nat, T ⊗^{ V}_{l} colimIn (free_monoid_coeq_sequence_colim_on A) n).
proof: Proof. intros m n e. etrans. do 2 apply cancel_postcomposition. apply (bifunctor_rightid V). etrans. apply cancel_postcomposition. apply id_left. etrans. apply (pathsinv0 (bifunctor_leftcomp V _ _ _ _ _ _)). apply maponpaths. set (colimA := free_monoid_coeq_sequence_colim_on A). apply pathsinv0. etrans. exact (pathsinv0 (colimInCommutes colimA _ _ e)). induction e. 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