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