Definition comp_preserves_fiberwise_initial {C₁ C₂ C₃ : category} {F : C₁ ⟶ C₂} {G : C₂ ⟶ C₃} {D₁ : disp_cat C₁} {D₂ : disp_cat C₂} {D₃ : disp_cat C₃} {FF : disp_functor F D₁ D₂} (HFF : preserves_fiberwise_initial FF) {GG : disp_functor G D₂ D₃} (HGG : preserves_fiberwise_initial GG) : preserves_fiberwise_initial (disp_functor_composite FF GG). Proof. intros x y Hy ; cbn. apply HGG. apply HFF. exact Hy. 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.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.Preservation.