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. 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.
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.