proposition: Lemma isColimCocone_pair_functor {gr : graph} (HF : ∏ (d : diagram gr A) (c : A) (cc : cocone d c) (h : isColimCocone d c cc), isColimCocone _ _ (mapcocone F d cc)) (HG : ∏ (d : diagram gr B) (c : B) (cc : cocone d c) (h : isColimCocone d c cc), isColimCocone _ _ (mapcocone G d cc)) : ∏ (d : diagram gr (category_binproduct A B)) (cd : A × B) (cc : cocone d cd), isColimCocone _ _ cc -> isColimCocone _ _ (mapcocone (pair_functor F G) d cc).
proof: Proof. intros cAB ml ccml Hccml xy ccxy. transparent assert (cFAX : (cocone (mapdiagram F (mapdiagram (pr1_functor A B) cAB)) (pr1 xy))). { use make_cocone. - intro n; apply (pr1 (pr1 ccxy n)). - abstract (intros m n e; apply (maponpaths dirprod_pr1 (pr2 ccxy m n e))). } transparent assert (cGBY : (cocone (mapdiagram G (mapdiagram (pr2_functor A B) cAB)) (pr2 xy))). { use make_cocone. - intro n; apply (pr2 (pr1 ccxy n)). - abstract (intros m n e; apply (maponpaths dirprod_pr2 (pr2 ccxy m n e))). } destruct (HF _ _ _ (isColimCocone_pr1_functor cAB ml ccml Hccml) _ cFAX) as [[f hf1] hf2]. destruct (HG _ _ _ (isColimCocone_pr2_functor cAB ml ccml Hccml) _ cGBY) as [[g hg1] hg2]. unfold is_cocone_mor in *. simpl in *. use tpair. - apply (tpair _ (f,,g)). abstract (intro n; unfold catbinprodmor, compose; simpl; now rewrite hf1, hg1). - abstract (intro t; apply subtypePath; simpl; [ intro x; apply impred; intro; apply isaset_dirprod; apply homset_property | induction t as [[f1 f2] p]; simpl in *; apply pathsdirprod; [ apply (maponpaths pr1 (hf2 (f1,, (λ n, maponpaths pr1 (p n))))) | apply (maponpaths pr1 (hg2 (f2,, (λ n, maponpaths dirprod_pr2 (p n)))))]]). 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