Definition pb_lift_1cell_factor : lift_1cell_factor DD hf gg. Proof. simple refine (_ ,, (_ ,, _) ,, _). - use make_disp_map_bicat_mor. + exact (pb_1cell_1cell φ). + exact (pred_mor_closed_under_pb_ump_mor D _ _ _ _ _ _ _ _ _ Hpb other_cone _ _ _ _ _ Hg Hp₁ (pr12 gg)). + exact (inv_of_invertible_2cell (pb_1cell_pr2 φ)). - exact (pb_1cell_pr1 φ). - abstract (cbn ; pose (pb_1cell_eq φ) as q ; cbn in q ; rewrite lwhisker_id2, id2_left ; rewrite !vassocl ; do 4 (use vcomp_move_R_pM ; [ is_iso | ] ; cbn) ; rewrite q ; rewrite !vassocl ; apply maponpaths ; refine (!_) ; etrans ; [ do 4 apply maponpaths ; rewrite !vassocr ; rewrite rassociator_lassociator ; rewrite id2_left ; rewrite !vassocl ; apply idpath | ] ; etrans ; [ do 3 apply maponpaths ; rewrite !vassocr ; rewrite rwhisker_vcomp ; rewrite vcomp_linv ; rewrite id2_rwhisker, id2_left ; apply idpath | ] ; etrans ; [ do 2 apply maponpaths ; rewrite !vassocr ; rewrite lassociator_rassociator, id2_left ; apply idpath | ] ; rewrite vcomp_linv ; apply id2_right). - apply is_invertible_to_is_disp_invertible. 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.CategoryTheory.DisplayedCats.StreetFibration. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Morphisms.FullyFaithful. Require Import UniMath.Bicategories.Morphisms.InternalStreetFibration. Require Import UniMath.Bicategories.Morphisms.InternalStreetOpFibration. Require Import UniMath.Bicategories.Logic.DisplayMapBicat. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.CleavingOfBicat. Require Import UniMath.Bicategories.DisplayedBicats.Examples.DisplayMapBicatToDispBicat. Require Import UniMath.Bicategories.Limits.Pullbacks.