proposition: Lemma rt_chain_isos_commute (A : C) (v : vertex nat_graph) : dmor (rightwhisker_chain_with A (free_monoid_coeq_sequence_diagram_on I_{ V})) (idpath (S v)) · z_iso_mor (rt_chain_isos A (S v)) = z_iso_mor (rt_chain_isos A v) · dmor (free_monoid_coeq_sequence_diagram_on A) (idpath (S v)).
proof: Proof. apply pathsinv0. apply (rt_chain_iso_pair_rel_impl_total_rel). exact (rtisp_rel (rt_chain_iso_pairs A v)). 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