Definition bincoproducts_cod_fib {C : category} (y : C) (H : BinCoproducts C) : BinCoproducts (C/y). Proof. intros f g. pose (coprod := H (cod_dom f) (cod_dom g)). use make_BinCoproduct. - exact (cod_fib_coproduct_ob f g coprod). - exact (cod_fib_coproduct_in1 f g coprod). - exact (cod_fib_coproduct_in2 f g coprod). - use to_bincoproduct_slice. exact (isBinCoproduct_BinCoproduct _ coprod). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod.