Definition lift_1cell_to_pb_1cell (Hg : lift_1cell_factor (cod_disp_bicat B) (π,, p) hg) : pb_1cell other_cone pb. Proof. use make_pb_1cell. - exact (pr11 Hg). - use inv_of_invertible_2cell. exact (pr21 Hg). - use make_invertible_2cell. + exact (pr112 Hg). + exact (pr21 (cod_disp_invertible_invertible_2_cell _ (pr2 Hg))). - abstract (pose (pr212 Hg) as q ; cbn ; cbn in q ; rewrite lwhisker_id2 in q ; rewrite id2_left in q ; rewrite !vassocl ; do 3 (use vcomp_move_L_pM ; [ is_iso | ] ; cbn) ; refine (_ @ maponpaths (λ z, z • _) q) ; clear q ; rewrite !vassocl ; do 3 apply maponpaths ; rewrite !(maponpaths (λ z, _ • (_ • z)) (vassocr _ _ _)) ; rewrite rwhisker_vcomp ; pose (maponpaths pr1 (disp_vcomp_rinv (pr2 Hg))) as q0 ; assert (q : pr1 (pr2 Hg •• disp_inv_cell (pr2 Hg)) = id₂ (pr11 Hg · π)) ; [ etrans; [exact q0 |] ; unfold transportb ; cbn ; etrans ; [ refine (pr1_transportf (! id2_left (id₂ (g · f))) (id₂ (pr11 Hg · π),, disp_id2 _)) |] ; cbn ; rewrite transportf_const ; apply idpath | refine (!_) ; etrans ; [ do 2 apply maponpaths ; apply maponpaths_2 ; apply maponpaths ; exact q | ] ; rewrite id2_rwhisker, id2_left ; rewrite lassociator_rassociator ; apply id2_right ] ). 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.