Definition preserves_global_lifts_to_cartesian {B : bicat} {D₁ : disp_bicat B} {D₂ : disp_bicat B} (HB : is_univalent_2 B) (HD₂ : disp_univalent_2 D₂) (HD₁ : global_cleaving D₁) {FF : disp_psfunctor D₁ D₂ (id_psfunctor _)} (HFF : preserves_global_lifts HD₁ FF) : global_cartesian_disp_psfunctor FF. Proof. intros b₁ b₂ f bb₁ bb₂ ff Hff. refine (invertible_2cell_from_cartesian HB (pr2 HD₂) _ (pr2 (disp_psfunctor_invertible_2cell FF (map_between_cartesian_1cell_commute (pr2 HB) ff (pr22 (HD₁ b₁ b₂ bb₂ f)))))). use (invertible_2cell_from_cartesian HB (pr2 HD₂) _ (pr2 (disp_psfunctor_comp _ _ _ _ _ _))). use (comp_cartesian_1cell HB). - exact (cartesian_1cell_disp_adj_equiv HB (pr1 HD₂) (@disp_psfunctor_id_on_disp_adjequiv _ _ _ FF _ _ (_ ,, pr1 (disp_adj_equiv_between_cartesian_1cell (pr2 HB) Hff (pr22 (HD₁ b₁ b₂ bb₂ f)))) _ _ _ (pr2 (disp_adj_equiv_between_cartesian_1cell (pr2 HB) Hff (pr22 (HD₁ b₁ b₂ bb₂ f)))))). - apply HFF. 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.CategoryTheory.DisplayedCats.Examples.Opposite. 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.Core.TransportLaws. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.CategoryTheory.DisplayedCats.Core. 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.DispPseudofunctor. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.Display.StrictPseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Import PseudoFunctor.Notations. Require Import UniMath.Bicategories.PseudoFunctors.StrictPseudoFunctor. Require Import UniMath.Bicategories.PseudoFunctors.Examples.StrictToPseudo. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Projection. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Identity. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Composition. Require Import UniMath.Bicategories.DisplayedBicats.CleavingOfBicat. Require Import UniMath.Bicategories.DisplayedBicats.Cartesians. Require Import UniMath.Bicategories.DisplayedBicats.EquivalenceBetweenCartesians.