Proposition preserves_binproduct_fiber_disp_codomain_functor {C₁ C₂ : category} (F : C₁ ⟶ C₂) (HF : preserves_pullback F) (x : C₁) : preserves_binproduct (fiber_functor (disp_codomain_functor F) x). Proof. intros y₁ y₂ z π₁ π₂ H. use isPullback_to_isBinProduct_cod_fib. apply isBinProduct_to_isPullback_cod_fib in H. use (isPullback_mor_paths _ _ _ _ _ _ (HF _ _ _ _ _ _ _ _ _ _ H)). - apply idpath. - apply idpath. - rewrite disp_codomain_fiber_functor_mor. apply idpath. - rewrite disp_codomain_fiber_functor_mor. apply idpath. - rewrite <- !functor_comp. apply maponpaths. exact (fib_isPullback π₁ π₂). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodLimits. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodColimits. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations.