Definition comp_preserves_dependent_products {C₁ C₂ C₃ : category} {D₁ : disp_cat C₁} {HD₁ : cleaving D₁} {D₂ : disp_cat C₂} {HD₂ : cleaving D₂} {D₃ : disp_cat C₃} {HD₃ : cleaving D₃} {F : C₁ ⟶ C₂} {G : C₂ ⟶ C₃} {FF : cartesian_disp_functor F D₁ D₂} {GG : cartesian_disp_functor G D₂ D₃} {P₁ : has_dependent_products HD₁} {P₂ : has_dependent_products HD₂} {P₃ : has_dependent_products HD₃} (HFF : preserves_dependent_products FF P₁ P₂) (HGG : preserves_dependent_products GG P₂ P₃) : preserves_dependent_products (comp_cartesian_disp_functor FF GG) P₁ P₃. Proof. intros x y f a. use (is_z_isomorphism_path (!(right_beck_chevalley_nat_trans_comp FF GG f a (pr1 P₁ _ _ f) (pr1 P₂ _ _ (#F f)) (pr1 P₃ _ _ (#G (#F f)))))). use is_z_isomorphism_comp. - use functor_on_is_z_isomorphism. apply HFF. - apply HGG. Defined.
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.