proposition: Lemma Products_from_Lims : Lims_of_shape I_graph C -> Products I C.
proof: Proof. intros H F. set (HF := H (products_diagram F)). use make_Product. + apply (lim HF). + intros i; apply (limOut HF). + apply (make_isProduct _ _ C); intros c Fic. use unique_exists. - apply limArrow. use make_cone. * simpl; intro i; apply Fic. * abstract (simpl; intros u v e; induction e). - abstract (simpl; intro i; apply (limArrowCommutes HF)). - abstract (intros y; apply impred; intro i; apply C). - abstract (intros f Hf; apply limArrowUnique; simpl in *; intros i; apply Hf). Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.ProductCategory UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.Combinatorics.StandardFiniteSets