proposition: Lemma isColimCocone_family_functor {gr : graph} (F : ∏ (i : I), functor A B) (HF : ∏ i (d : diagram gr A) (c : A) (cc : cocone d c) (h : isColimCocone d c cc), isColimCocone _ _ (mapcocone (F i) d cc)) : ∏ (d : diagram gr (product_category (λ _, A))) (cd : I -> A) (cc : cocone d cd), isColimCocone _ _ cc -> isColimCocone _ _ (mapcocone (family_functor I F) d cc).
proof: Proof. intros cAB ml ccml Hccml xy ccxy; simpl in *. transparent assert (cc : (∏ i, cocone (mapdiagram (F i) (mapdiagram (pr_functor I (λ _ : I, A) i) cAB)) (xy i))). { intro i; use make_cocone. - intro n; use (pr1 ccxy n). - abstract (intros m n e; apply (toforallpaths _ _ _ (pr2 ccxy m n e) i)). } set (X i := HF i _ _ _ (isColimCocone_pr_functor _ _ _ Hccml i) (xy i) (cc i)). use tpair. - use tpair. + intro i; apply (pr1 (pr1 (X i))). + abstract (intro n; apply funextsec; intro j; apply (pr2 (pr1 (X j)) n)). - abstract (intro t; apply subtypePath; simpl; [ intro x; apply impred; intro; apply impred_isaset; intro i; apply homset_property | destruct t as [f1 f2]; simpl in *; apply funextsec; intro i; transparent assert (H : (∑ x : B ⟦ (F i) (ml i), xy i ⟧, ∏ n, # (F i) (coconeIn ccml n i) · x = coconeIn ccxy n i)); [apply (tpair _ (f1 i)); intro n; apply (toforallpaths _ _ _ (f2 n) i)|]; apply (maponpaths pr1 (pr2 (X i) H))]). Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Slice UniMath.CategoryTheory.Categories.HSET.Limits UniMath.CategoryTheory.Categories.HSET.Colimits UniMath.CategoryTheory.Categories.HSET.Structures UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.ProductCategory UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Adjunctions.Examples UniMath.CategoryTheory.exponentials UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.RightKanExtension UniMath.CategoryTheory.slicecat UniMath.CategoryTheory.Chains.Chains