proposition: Lemma isLimCone_in_product_category {g : graph} (c : diagram g (product_category B)) (b : product_precategory B) (cc : cone c b) (M : ∏ i, isLimCone _ _ (mapcone (pr_functor I B i) _ cc)) : isLimCone 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; set (MM := M i _ (mapcone (pr_functor I B i) _ cc')); set (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 _ (mapcone (pr_functor I B i) _ cc')))). + abstract ( intros v; apply funextsec; intros i; use (pr2 (pr1 (M i _ (mapcone (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.Limits UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Slice UniMath.CategoryTheory.Categories.HSET.Limits UniMath.CategoryTheory.Categories.HSET.Limits UniMath.CategoryTheory.Categories.HSET.Structures UniMath.CategoryTheory.opp_precat 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.Colimits 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 UniMath.CategoryTheory.Chains.Cochains UniMath.CategoryTheory.OppositeCategory.Core UniMath.CategoryTheory.OppositeCategory.LimitsAsColimits UniMath.CategoryTheory.OppositeCategory.OppositeOfFunctorCategory UniMath.CategoryTheory.Chains.OmegaCocontFunctors UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.Equivalences.CompositesAndInverses