Definition slice_coprod_ump_2 : bincoprod_ump_2 slice_coprod_cone. Proof. intros q φ ψ α β. use iscontraprop1. - exact (slice_coprod_ump_unique α β). - simple refine ((_ ,, _) ,, _ ,, _). + exact (bincoprod_ump_2cell ump (pr1 α) (pr1 β)). + cbn. use (bincoprod_ump_2cell_unique_alt ump). * abstract (rewrite <- lwhisker_vcomp ; use (vcomp_rcancel (lassociator _ _ _)) ; [ is_iso | ] ; rewrite !vassocl ; rewrite rwhisker_lwhisker ; rewrite bincoprod_ump_2cell_inl ; use (vcomp_lcancel ((bincoprod_ump_1cell_inl ump b h₁ h₂) ^-1)) ; [ is_iso | ] ; rewrite !vassocr ; pose (pr2 α) as p ; cbn in p ; rewrite !vassocr in p ; exact p). * abstract (rewrite <- lwhisker_vcomp ; use (vcomp_rcancel (lassociator _ _ _)) ; [ is_iso | ] ; rewrite !vassocl ; rewrite rwhisker_lwhisker ; rewrite bincoprod_ump_2cell_inr ; use (vcomp_lcancel ((bincoprod_ump_1cell_inr ump b h₁ h₂) ^-1)) ; [ is_iso | ] ; rewrite !vassocr ; pose (pr2 β) as p ; cbn in p ; rewrite !vassocr in p ; exact p). + abstract (use eq_2cell_slice ; cbn ; apply (bincoprod_ump_2cell_inl ump)). + abstract (use eq_2cell_slice ; cbn ; apply (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.CategoryTheory.DisplayedCats.Core. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Slice. Require Import UniMath.Bicategories.Colimits.Initial. Require Import UniMath.Bicategories.Colimits.Coproducts.