Lemma isaprop_BinCoproductCocone : isaprop (BinCoproductCocone a b). Proof. apply invproofirrelevance. intros CC CC'. apply subtypePath. + intros. unfold isColimCocone. do 2 (apply impred; intro); apply isapropiscontr. + apply (total2_paths_f (isotoid _ H (iso_from_BinCoproduct_to_BinCoproduct CC CC'))). rewrite transportf_dirprod. rewrite transportf_isotoid'. simpl. rewrite transportf_isotoid'. destruct CC as [CC bla]. destruct CC' as [CC' bla']; simpl in *. destruct CC as [CC [CC1 CC2]]. destruct CC' as [CC' [CC1' CC2']]; simpl in *. unfold from_BinCoproduct_to_BinCoproduct. rewrite BinCoproductIn1Commutes. rewrite BinCoproductIn2Commutes. apply idpath. Qed.
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.