Definition is_pb_to_cartesian_lift_2cell : lift_2cell_factor (cod_disp_bicat B) (π,, p) σσ Lh Lh'. Proof. use iscontraprop1. - exact is_pb_to_cartesian_lift_2cell_unique. - simple refine (_ ,, _). + exact is_pb_to_cartesian_lift_2cell_disp_cell. + abstract (use subtypePath ; [ intro ; apply cellset_property | ] ; etrans ; [ exact (transportf_cell_of_cod_over _ _) | ] ; simpl ; etrans ; [ apply maponpaths_2 ; apply (pb_ump_cell_pr2 pb_sqr) | ] ; do 2 refine (vassocl _ _ _ @ _) ; apply maponpaths ; refine (_ @ id2_right _) ; apply maponpaths ; apply (pr2 ℓπ')). 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.