Definition binprod_2_ump_in_disp_map_slice_cell : φ ==> ψ. Proof. simple refine (_ ,, _). - use (pb_ump_cell Hpb _ _ (pr1 α) (pr1 β)) ; cbn. abstract (pose (r₁ := pr2 α) ; pose (r₂ := pr2 β) ; cbn in r₁, r₂ ; rewrite !lwhisker_id2, !id2_left in r₁ ; use (vcomp_lcancel (pr22 φ)) ; [ apply property_from_invertible_2cell | ] ; rewrite !vassocr ; rewrite !vassocr in r₂ ; refine (maponpaths (λ z, z • _) r₂ @ _) ; clear r₂ ; refine (_ @ maponpaths (λ z, (z • _) • _) (!r₁)) ; clear r₁ ; rewrite !vassocl ; apply maponpaths ; rewrite lassociator_rassociator, id2_right ; rewrite !vassocr ; rewrite lassociator_rassociator, id2_left ; apply idpath). - abstract (cbn ; use (vcomp_rcancel (lassociator _ _ _)) ; [ is_iso | ] ; rewrite !vassocl ; rewrite <- rwhisker_rwhisker ; rewrite (pb_ump_cell_pr1 Hpb) ; pose (pr2 α) as r ; cbn in r ; rewrite !lwhisker_id2, !id2_left in r ; rewrite !vassocr ; exact r). 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.DisplayMapBicatSlice. Require Import UniMath.Bicategories.Limits.Final. Require Import UniMath.Bicategories.Limits.Products. Require Import UniMath.Bicategories.Limits.Pullbacks. Require Import UniMath.Bicategories.Limits.Examples.OpCellBicatLimits. Require Import UniMath.Bicategories.Logic.DisplayMapBicat.