Definition binprod_1_ump_in_disp_map_slice_cell : binprod_1cell q binprod_cone_in_disp_map_slice. Proof. use make_binprod_1cell. - simple refine (_ ,, _ ,, _) ; cbn. + exact (pb_ump_mor Hpb other_cone). + use (invertible_pred_mor_1 _ (inv_of_invertible_2cell (pr22 (binprod_cone_pr1 q)))). apply (D_mor _ _ _ _ _ _ _ _ _ Hpb _ _ _ (comp_of_invertible_2cell (inv_of_invertible_2cell (pr22 (binprod_cone_pr1 q))) (pr22 (binprod_cone_pr2 q))) Hf). * exact (invertible_pred_mor_1 _ (pr22 (binprod_cone_pr1 q)) (pr12 (binprod_cone_pr1 q))). * exact (invertible_pred_mor_1 _ (pr22 (binprod_cone_pr1 q)) (pr12 (binprod_cone_pr2 q))). + exact φ. - use make_invertible_2cell. + simple refine (_ ,, _). * exact (pb_ump_mor_pr1 Hpb other_cone). * abstract (cbn ; rewrite lwhisker_id2, id2_left ; rewrite !vassocl ; rewrite !(maponpaths (λ z, _ • (_ • z)) (vassocr _ _ _)) ; rewrite rassociator_lassociator ; rewrite id2_left ; rewrite rwhisker_vcomp ; rewrite vcomp_linv ; rewrite id2_rwhisker ; apply id2_right). + use is_invertible_2cell_in_disp_map_slice_bicat. apply property_from_invertible_2cell. - use make_invertible_2cell. + simple refine (_ ,, _). * exact (pb_ump_mor_pr2 Hpb other_cone). * apply binprod_1_ump_in_disp_map_slice_cell_eq. + use is_invertible_2cell_in_disp_map_slice_bicat. apply property_from_invertible_2cell. 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.