proposition: Lemma nwfs_closed_coproducts {C : category} {I : hSet} (n : nwfs C) {a b : I -> C} {f : ∏ (i : I), a i --> b i} (hf : ∏ (i : I), (nwfs_L_maps n (f i))) (CCa : Coproduct _ _ a) (CCb : Coproduct _ _ b) : nwfs_L_maps n (CoproductOfArrows _ _ CCa CCb f).
proof: Proof. transparent assert (ini : (∏ i, f i --> CoproductOfArrows I C CCa CCb f)). { intro i. use mors_to_arrow_mor. - exact (CoproductIn _ _ CCa i). - exact (CoproductIn _ _ CCb i). - abstract (apply CoproductInCommutes). } use tpair. - use mors_to_arrow_mor. * exact (identity _). * use CoproductArrow. intro i. apply (compose (arrow_mor11 (pr1 (hf i)))). exact (three_mor11 (#(fact_functor n) (ini i))). * abstract ( etrans; [apply id_left|]; use CoproductArrow_eq; intro i; etrans; [exact (pathsinv0 (pr1 (three_mor_comm (#(fact_functor n) (ini i)))))|]; apply pathsinv0; etrans; [apply assoc|]; etrans; [apply cancel_postcomposition; apply CoproductOfArrows'In|]; etrans; [apply assoc'|]; etrans; [apply cancel_precomposition; apply CoproductInCommutes|]; etrans; [apply assoc|]; apply cancel_postcomposition; etrans; [exact (pathsinv0 (arrow_mor_comm (pr1 (hf i))))|]; etrans; [apply cancel_postcomposition; etrans; [exact (pathsinv0 (id_right _))|]; exact (arrow_mor00_eq (pr12 (hf i)))|]; apply id_left ). - split. * use arrow_mor_eq; [apply id_left|]. use CoproductArrow_eq. intro i. etrans. apply assoc. etrans. apply cancel_postcomposition. use (CoproductInCommutes). etrans. apply assoc'. etrans. apply cancel_precomposition. exact (pathsinv0 (pr2 (three_mor_comm (#(fact_functor n) (ini i))))). etrans. apply assoc. etrans. apply cancel_postcomposition. exact (arrow_mor11_eq (pr12 (hf i))). etrans. apply id_left. apply pathsinv0. apply id_right. * use arrow_mor_eq. + apply cancel_precomposition. exact (nwfs_Σ_top_map_id n (CoproductOfArrows I C CCa CCb f)). + use CoproductArrow_eq. intro i. etrans. apply assoc. etrans. apply cancel_postcomposition. apply CoproductInCommutes. etrans. apply assoc'. etrans. apply cancel_precomposition. { set (Σnat := nat_trans_ax (nwfs_Σ n) _ _ (ini i)). exact (arrow_mor11_eq Σnat). } etrans. apply assoc. etrans. apply cancel_postcomposition. exact (arrow_mor11_eq (pr22 (hf i))). etrans. apply assoc'. apply pathsinv0. etrans. apply assoc. etrans. apply cancel_postcomposition. apply CoproductInCommutes. etrans. apply assoc'. apply cancel_precomposition. etrans. apply (pr1_section_disp_on_morphisms_comp). apply pathsinv0. etrans. apply (pr1_section_disp_on_morphisms_comp). use (section_disp_on_eq_morphisms). -- etrans. apply cancel_postcomposition. etrans. exact (pathsinv0 (id_right _)). exact (arrow_mor00_eq (pr12 (hf i))). etrans. apply id_left. apply pathsinv0. apply id_right. -- apply pathsinv0. etrans. apply (CoproductInCommutes I C _ CCb). reflexivity. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.Monads.MonadAlgebras UniMath.CategoryTheory.Monads.Comonads UniMath.CategoryTheory.Monads.ComonadCoalgebras UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Chains.Chains UniMath.CategoryTheory.DisplayedCats.Examples.Arrow UniMath.CategoryTheory.DisplayedCats.Examples.Three UniMath.ModelCategories.MorphismClass UniMath.ModelCategories.Retract UniMath.ModelCategories.Lifting UniMath.ModelCategories.WFS UniMath.ModelCategories.NWFS UniMath.ModelCategories.Helpers