Proposition preserves_bincoproduct_fiber_disp_codomain_functor {C₁ C₂ : category} (HC₁ : BinCoproducts C₁) (F : C₁ ⟶ C₂) (HF : preserves_bincoproduct F) (x : C₁) : preserves_bincoproduct (fiber_functor (disp_codomain_functor F) x). Proof. use preserves_bincoproduct_if_preserves_chosen. - exact (bincoproducts_cod_fib x HC₁). - intros y₁ y₂. use to_bincoproduct_slice. pose (HC₁ (cod_dom y₁) (cod_dom y₂)) as coprod. pose (HF _ _ _ _ _ (isBinCoproduct_BinCoproduct _ coprod)) as Fcoprod. use (isBinCoproduct_eq_arrow _ _ Fcoprod). + abstract (rewrite disp_codomain_fiber_functor_mor ; apply idpath). + abstract (rewrite disp_codomain_fiber_functor_mor ; apply idpath). Defined.
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.