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).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Limits.Pullbacks.