Lemma isColimCocone_in_product_category {g : graph} (c : diagram g (product_category B)) (b : product_precategory B) (cc : cocone c b) (M : ∏ i, isColimCocone _ _ (mapcocone (pr_functor I B i) _ cc)) : isColimCocone c b cc. Proof. intros b' cc'. apply iscontraprop1. - abstract ( apply invproofirrelevance; intros f1 f2; apply subtypePath; [ intros f; apply impred_isaprop; intros v; apply has_homsets_product_precategory | ]; apply funextsec; intros i; assert (MM := M i _ (mapcocone (pr_functor I B i) _ cc')); assert (H := proofirrelevancecontr MM); use (maponpaths pr1 (H (pr1 f1 i,,_) (pr1 f2 i,,_))); clear MM H; intros v ; [ exact (toforallpaths _ _ _ (pr2 f1 v) i) | exact (toforallpaths _ _ _ (pr2 f2 v) i) ] ) . - use tpair. + intros i. use (pr1 (pr1 (M i _ (mapcocone (pr_functor I B i) _ cc')))). + abstract ( intros v; apply funextsec; intros i; use (pr2 (pr1 (M i _ (mapcocone (pr_functor I B i) _ cc'))) v) ). 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.