Definition z_iso_between_Product {C : category} {J : UU} {D : J → C} (prod₁ prod₂ : Product J C D) : z_iso prod₁ prod₂. Proof. use make_z_iso. - exact (ProductArrow _ _ prod₂ (ProductPr _ _ prod₁)). - exact (ProductArrow _ _ prod₁ (ProductPr _ _ prod₂)). - split. + abstract (use ProductArrow_eq ; intro j ; rewrite !assoc' ; rewrite !ProductPrCommutes ; rewrite id_left ; apply idpath). + abstract (use ProductArrow_eq ; intro j ; rewrite !assoc' ; rewrite !ProductPrCommutes ; rewrite id_left ; apply idpath). 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.