fact: Definition preserves_dependent_sums {C₁ C₂ : category} {D₁ : disp_cat C₁} {HD₁ : cleaving D₁} {D₂ : disp_cat C₂} {HD₂ : cleaving D₂} {F : C₁ ⟶ C₂} (FF : cartesian_disp_functor F D₁ D₂) (L₁ : has_dependent_sums HD₁) (L₂ : has_dependent_sums HD₂) : UU := ∏ (x y : C₁) (f : x --> y) (a : D₁[{x}]), is_z_isomorphism (left_beck_chevalley_nat_trans (pr1 L₁ x y f) (pr1 L₂ (F x) (F y) (#F f)) (nat_z_iso_inv (fiber_functor_natural_nat_z_iso HD₁ HD₂ FF f)) a).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Fibrations UniMath.CategoryTheory.DisplayedCats.Fiber UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Limits.Pullbacks