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₂ e f g h p q H. use (isEqualizer_eq _ _ _ _ _ (HGG _ _ _ _ _ _ _ _ _ (HFF _ _ _ _ _ _ _ _ _ H))). - abstract (cbn in q ; cbn ; rewrite !disp_functor_transportf ; rewrite !mor_disp_transportf_prewhisker ; rewrite !mor_disp_transportf_prewhisker in q ; rewrite !mor_disp_transportf_postwhisker ; rewrite !mor_disp_transportf_postwhisker in q ; rewrite !transport_f_f ; rewrite !transport_f_f in q ; refine (_ @ q @ _) ; apply maponpaths_2 ; apply homset_property). - abstract (cbn ; rewrite disp_functor_transportf ; rewrite transport_f_f ; apply idpath). - abstract (cbn ; rewrite disp_functor_transportf ; rewrite transport_f_f ; apply idpath). - abstract (cbn ; rewrite disp_functor_transportf ; rewrite transport_f_f ; apply idpath). - abstract (cbn ; rewrite !mor_disp_transportf_prewhisker ; rewrite !mor_disp_transportf_postwhisker ; rewrite <- !disp_functor_comp_var ; rewrite !transport_f_f ; do 2 apply maponpaths ; cbn in p ; refine (!_ @ maponpaths (λ z, transportb (λ f, _ -->[ f ] _) _ z) p @ _) ; apply transportbfinv). 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.Equalizers. Require Import UniMath.CategoryTheory.Limits.Preservation.