proposition: Lemma rt_chain_iso_pairs (A : C) (v : vertex nat_graph) : rt_chain_iso_pair A v.
proof: Proof. induction v as [|v Cisv]. - use make_rt_chain_iso_pair. * exact (_,, _,, monoidal_leftunitorisolaw V A). * exact (_,, is_z_iso_rightwhiskering_z_iso V A _ (_,, monoidal_rightunitorisolaw V T)). * abstract ( etrans; [apply cancel_postcomposition; apply (bifunctor_rightid V)|]; etrans; [apply id_left|]; apply pathsinv0; etrans; [apply id_right|]; apply (monoidal_triangleidentity V) ). - set (coeq := next_pair_diagram_coeq (free_monoid_coeq_sequence_on I_{V} v)). set (rt_coequalizer := rt_coeq_coequalizer (rt_coeq A) coeq). use make_rt_chain_iso_pair. * exact (rtisp_riso Cisv). * use make_z_iso. + use (CoequalizerOut _ rt_coequalizer). -- apply (compose (α^{V}_{_, _, _})). apply (compose (T ⊗^{V}_{l} (z_iso_mor (rtisp_riso Cisv)))). exact (CoequalizerArrow _ (next_pair_diagram_coeq (free_monoid_coeq_sequence_on A v))). -- exact (rt_chain_iso_pair_ind_iscoeqout A v Cisv). + use CoequalizerOut. -- apply (compose (T ⊗^{V}_{l} (z_iso_inv (rtisp_riso Cisv)))). apply (compose (αinv^{V}_{_, _, _})). exact ((CoequalizerArrow _ (next_pair_diagram_coeq (free_monoid_coeq_sequence_on I_{V} v))) ⊗^{V}_{r} A). -- exact (rt_chain_iso_pair_ind_inv_iscoeqout A v Cisv). + split. -- abstract ( apply pathsinv0; use (CoequalizerEndo_is_identity _ rt_coequalizer); etrans; [apply assoc|]; etrans; [apply cancel_postcomposition; apply (CoequalizerArrowComm _ rt_coequalizer)|]; etrans; [apply cancel_postcomposition, assoc|]; etrans; [apply assoc'|]; etrans; [apply cancel_precomposition; apply (CoequalizerArrowComm)|]; etrans; [apply assoc|]; etrans; [apply assoc|]; etrans; [apply cancel_postcomposition|]; [ etrans; [apply assoc4|]; etrans; [apply cancel_postcomposition, cancel_precomposition; etrans; [exact (pathsinv0 (bifunctor_leftcomp V _ _ _ _ _ _))|]; etrans; [apply maponpaths; exact (pr122 (pr12 Cisv))|]; apply (bifunctor_leftid V)|]; etrans; [apply cancel_postcomposition, id_right|]; apply (monoidal_associatorisolaw V) |]; apply id_left ). -- abstract ( apply pathsinv0; use (CoequalizerEndo_is_identity); etrans; [apply assoc|]; etrans; [apply cancel_postcomposition; apply (CoequalizerArrowComm)|]; etrans; [apply cancel_postcomposition, assoc|]; etrans; [apply assoc'|]; etrans; [apply cancel_precomposition; apply (CoequalizerArrowComm _ rt_coequalizer)|]; etrans; [apply assoc|]; etrans; [apply assoc|]; etrans; [apply cancel_postcomposition|]; [ etrans; [apply assoc4|]; etrans; [apply cancel_postcomposition, cancel_precomposition; apply (monoidal_associatorisolaw V)|]; etrans; [apply cancel_postcomposition, id_right|]; etrans; [exact (pathsinv0 (bifunctor_leftcomp V _ _ _ _ _ _))|]; etrans; [apply maponpaths; exact (pr222 (rtisp_riso Cisv))|]; apply (bifunctor_leftid V) |]; apply id_left ). * abstract ( etrans; [apply (CoequalizerArrowComm _ rt_coequalizer)|]; apply assoc ). 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