proposition: Lemma rt_chain_colim_iso (A : C) : z_iso (colim (free_monoid_coeq_sequence_rightwhisker_colim_on A I_{V})) (colim (free_monoid_coeq_sequence_colim_on A)).
proof: Proof. use make_z_iso. - use colimOfArrows. * intro v. exact (z_iso_mor (rt_chain_isos A v)). * abstract ( intros u v e; induction e; exact (rt_chain_isos_commute A u) ). - use colimOfArrows. * intro v. exact (z_iso_inv (rt_chain_isos A v)). * abstract ( intros u v e; induction e; apply (post_comp_with_z_iso_is_inj (pr22 (rt_chain_isos A (S u)))); etrans; [apply assoc'|]; etrans; [apply cancel_precomposition; exact (pr222 (rt_chain_isos A (S u)))|]; etrans; [apply id_right|]; apply (pre_comp_with_z_iso_is_inj (pr22 (rt_chain_isos A u))); apply pathsinv0; etrans; [apply assoc|]; etrans; [apply cancel_postcomposition, assoc|]; etrans; [apply assoc'|]; etrans; [apply cancel_postcomposition; exact (pr122 (rt_chain_isos A u))|]; etrans; [apply id_left|]; exact (rt_chain_isos_commute A u) ). - abstract ( split; apply pathsinv0; apply colim_endo_is_identity; intro v; ( etrans; [apply assoc|]; etrans; [apply cancel_postcomposition, colimOfArrowsIn|]; etrans; [apply assoc'|]; etrans; [apply cancel_precomposition, colimOfArrowsIn|]; etrans; [apply assoc|] ); [ etrans; [apply cancel_postcomposition; exact (pr122 (rt_chain_isos A v))|]; apply id_left | etrans; [apply cancel_postcomposition; exact (pr222 (rt_chain_isos A v))|]; apply id_left ] ). Defined.
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