Lemma Products_from_Lims : Lims_of_shape I_graph C -> Products I C. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.ProductCategory. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.Combinatorics.StandardFiniteSets. Section ProductFromIso. End ProductFromIso.