Definition global_cleaving_of_disp_map_bicat : global_cleaving DD. Proof. intros x y yy f. pose (pb := pb_ob_of_pred_ob D (pr12 yy) f (pr22 yy)). pose (p₁ := pb_pr1_of_pred_ob D (pr12 yy) f (pr22 yy)). pose (p₂ := pb_pr2_of_pred_ob D (pr12 yy) f (pr22 yy)). pose (γ := pb_cell_of_pred_ob D (pr12 yy) f (pr22 yy)). pose (ump := pb_of_pred_ob_has_pb_ump D (pr12 yy) f (pr22 yy)). pose (Hp₁ := mor_of_pb_preserves_pred_ob D (pr22 yy) ump). pose (Hp₂ := pb_preserves_pred_ob D (pr22 yy) ump). simple refine (_ ,, _ ,, _). - use make_disp_map_bicat_ob. + exact pb. + exact p₂. + exact Hp₂. - use make_disp_map_bicat_mor ; cbn. + exact p₁. + exact Hp₁. + exact (inv_of_invertible_2cell γ). - apply pb_to_cartesian_1cell. apply ump. 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.