Definition pb_1cell_to_lift_1cell (Hg : pb_1cell other_cone pb) : lift_1cell_factor (cod_disp_bicat B) (π,, p) hg. Proof. simple refine ((_ ,, _) ,, ((_ ,, _) ,, _)). - exact (pb_1cell_1cell Hg). - exact (inv_of_invertible_2cell (pb_1cell_pr1 Hg)). - exact (pr1 (pb_1cell_pr2 Hg)). - abstract (cbn ; pose (pb_1cell_eq Hg) as q ; cbn in q ; rewrite lwhisker_id2, id2_left ; rewrite !vassocl ; do 3 (use vcomp_move_R_pM ; [ is_iso | ] ; cbn) ; refine (maponpaths (λ z, z • _) q @ _) ; clear q ; rewrite !vassocl ; do 3 apply maponpaths ; refine (_ @ id2_right _) ; apply maponpaths ; use vcomp_move_R_pM ; [ is_iso | ] ; cbn ; rewrite !vassocr ; rewrite rassociator_lassociator ; rewrite id2_left, id2_right ; apply idpath). - use is_disp_invertible_2cell_cod. exact (pr2 (pb_1cell_pr2 Hg)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.whiskering. 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.Univalence. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Morphisms.InternalStreetFibration. Require Import UniMath.Bicategories.Morphisms.InternalStreetOpFibration. Require Import UniMath.Bicategories.Core.Examples.OneTypes. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.DisplayedBicats.CleavingOfBicat. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Codomain. Require Import UniMath.Bicategories.Limits.Pullbacks. Require Import UniMath.Bicategories.Limits.Examples.OneTypesLimits.