Lemma is_z_iso_from_BinCoproduct_to_BinCoproduct (CC CC' : BinCoproductCocone a b) : is_z_isomorphism (from_BinCoproduct_to_BinCoproduct CC CC'). Proof. exists (from_BinCoproduct_to_BinCoproduct CC' CC). split; simpl. - apply pathsinv0. apply BinCoproduct_endo_is_identity. + rewrite assoc. unfold from_BinCoproduct_to_BinCoproduct. rewrite BinCoproductIn1Commutes. rewrite BinCoproductIn1Commutes. apply idpath. + rewrite assoc. unfold from_BinCoproduct_to_BinCoproduct. rewrite BinCoproductIn2Commutes. rewrite BinCoproductIn2Commutes. apply idpath. - apply pathsinv0. apply BinCoproduct_endo_is_identity. + rewrite assoc; unfold from_BinCoproduct_to_BinCoproduct. repeat rewrite BinCoproductIn1Commutes; apply idpath. + rewrite assoc; unfold from_BinCoproduct_to_BinCoproduct. repeat rewrite BinCoproductIn2Commutes; apply idpath. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.EqDiag. Require Import UniMath.CategoryTheory.Limits.BinCoproducts.