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. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Slice. Require Import UniMath.CategoryTheory.Categories.HSET.Limits. Require Import UniMath.CategoryTheory.Categories.HSET.Colimits. Require Import UniMath.CategoryTheory.Categories.HSET.Structures. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.ProductCategory. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Adjunctions.Examples. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.RightKanExtension. Require Import UniMath.CategoryTheory.slicecat. Require Import UniMath.CategoryTheory.Chains.Chains.