proposition: Lemma Tinf_rightwhisker_inclusion_commutes (v : vertex nat_graph) : Tinf_rightwhisker_inclusion v · dmor (free_monoid_coeq_sequence_diagram_on I_{ V}) (idpath (S v)) ⊗^{V}_{r} Tinf = dmor (free_monoid_coeq_sequence_diagram_on I_{V}) (idpath (S v)) · Tinf_rightwhisker_inclusion (S v).
proof: Proof. etrans. apply assoc'. etrans. apply cancel_precomposition. exact (pathsinv0 (whiskerscommutes V (bifunctor_equalwhiskers V) _ _)). etrans. apply assoc. etrans. apply cancel_postcomposition. apply (monoidal_rightunitorinvnat V). apply assoc'. 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