Definition z_iso_between_Coproduct {C : category} {J : UU} {D : J → C} (coprod₁ coprod₂ : Coproduct J C D) : z_iso coprod₁ coprod₂. Proof. use make_z_iso. - exact (CoproductArrow _ _ coprod₁ (CoproductIn _ _ coprod₂)). - exact (CoproductArrow _ _ coprod₂ (CoproductIn _ _ coprod₁)). - split. + abstract (use CoproductArrow_eq ; intro j ; rewrite !assoc ; rewrite !CoproductInCommutes ; rewrite id_right ; apply idpath). + abstract (use CoproductArrow_eq ; intro j ; rewrite !assoc ; rewrite !CoproductInCommutes ; rewrite id_right ; 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.whiskering.