Definition local_cleaving_to_local_fib {B : bicat} {D : disp_bicat B} (HD : local_cleaving D) : local_fib D. Proof. intros x y xx yy g f α gg ; cbn in *. pose (HD x y xx yy f g gg α) as lift. unfold cartesian_lift. unfold cartesian_lift_2cell in lift. cbn. refine (pr1 lift ,, pr12 lift ,, _). apply cartesian_2cell_to_cartesian. exact (pr22 lift). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. 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.TransportLaws. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles.