proposition: Lemma Tinf_limit_step_colimIn_commutes (v : vertex nat_graph) : T ⊗^{ V}_{l} colimIn free_monoid_coeq_sequence_colim_unit (S v) · CoequalizerArrow C (free_monoid_coeq_sequence_limit_step_coeq I_{ V}) = CoequalizerArrow C (next_pair_diagram_coeq (free_monoid_coeq_sequence_on I_{V} v)) · colimIn free_monoid_coeq_sequence_colim_unit (S (S v)) · pair_diagram_horizontal_arrow (free_monoid_coeq_sequence_limit_ordinal_step_on I_{V}).
proof: Proof. show_id_type. set (coeq := free_monoid_coeq_sequence_limit_step_coeq I_{V}). set (limstepcomm := CoequalizerArrowEq _ coeq). set (TTinfin := colimIn (free_monoid_coeq_sequence_leftwhisker_colim_on T I_{ V}) (S v)). set (TTinfin_limstepcomm := cancel_precomposition _ _ _ _ _ _ TTinfin limstepcomm). use (pathscomp1 TTinfin_limstepcomm). - etrans. apply assoc. etrans. apply cancel_postcomposition. apply (colimArrowCommutes). reflexivity. - etrans. apply assoc. unfold top. etrans. apply cancel_postcomposition. { etrans. apply assoc. etrans. apply cancel_postcomposition. apply (colimArrowCommutes). etrans. apply assoc'. apply cancel_precomposition. etrans. apply assoc. etrans. apply cancel_postcomposition. apply (chain_shift_left_colimIn_commutes). reflexivity. } cbn. etrans. apply assoc'. apply pathsinv0. etrans. apply assoc'. apply cancel_precomposition. 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