Definition has_bincoprod_ump_2_op_cell : bincoprod_ump_2 op_cell_cocone. Proof. intros q φ ψ α β. use iscontraprop1. - abstract (use invproofirrelevance ; intros φ₁ φ₂ ; use subtypePath ; [ intro ; apply isapropdirprod ; apply cellset_property | ] ; exact (bincoprod_ump_2cell_unique_alt ump _ _ (pr12 φ₁ @ !(pr12 φ₂)) (pr22 φ₁ @ !(pr22 φ₂)))). - simple refine (_ ,, _ ,, _). + exact (bincoprod_ump_2cell ump α β). + exact (bincoprod_ump_2cell_inl ump α β). + exact (bincoprod_ump_2cell_inr ump α β). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Examples.OpCellBicat. Require Import UniMath.Bicategories.Morphisms.FullyFaithful. Require Import UniMath.Bicategories.Morphisms.Examples.MorphismsInOp2Bicat. Require Import UniMath.Bicategories.Colimits.Initial. Require Import UniMath.Bicategories.Colimits.Coproducts. Require Import UniMath.Bicategories.Colimits.Extensive. Require Import UniMath.Bicategories.Limits.Pullbacks. Require Import UniMath.Bicategories.Limits.CommaObjects. Require Import UniMath.Bicategories.Limits.Examples.OpCellBicatLimits.