Definition comp_preserves_fiberwise_binproducts {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_binproducts FF) {GG : disp_functor G D₂ D₃} (HGG : preserves_fiberwise_binproducts GG) : preserves_fiberwise_binproducts (disp_functor_composite FF GG). Proof. intros x y₁ y₂ z p q H. use (isBinProduct_eq_arrow _ _ (HGG _ _ _ _ _ _ (HFF _ _ _ _ _ _ H))) ; cbn. - abstract (rewrite disp_functor_transportf ; rewrite transport_f_f ; apply idpath). - abstract (rewrite disp_functor_transportf ; rewrite transport_f_f ; apply idpath). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. 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.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Preservation.