Definition functor_precat_product_cone : Product I [C, D] F. Proof. use make_Product. - apply product_of_functors. - apply product_nat_trans_pr. - use make_isProduct. + apply functor_category_has_homsets. + intros A f. use tpair. * apply (tpair _ (product_nat_trans A f)). abstract (intro i; apply (nat_trans_eq D); intro c; apply (ProductPrCommutes I D _ (HD (λ j, (F j) c)))). * abstract ( intro t; apply subtypePath; simpl; [intro; apply impred; intro; apply (isaset_nat_trans D)|]; apply (nat_trans_eq D); intro c; apply ProductArrowUnique; intro i; apply (nat_trans_eq_pointwise (pr2 t i))). 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.