Definition preserves_dependent_products {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₂) (R₁ : has_dependent_products HD₁) (R₂ : has_dependent_products HD₂) : UU := ∏ (x y : C₁) (f : x --> y) (a : D₁[{x}]), is_z_isomorphism (right_beck_chevalley_nat_trans (pr1 R₁ x y f) (pr1 R₂ (F x) (F y) (#F f)) (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.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentSums. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Limits.Pullbacks.