Definition total_BinCoproducts (PC : BinCoproducts C) (DC : disp_BinCoproducts PC) : BinCoproducts (total_category D). Proof. intros x y. use make_BinCoproduct. - exact (total_category_BinCoproduct x y (PC (pr1 x) (pr1 y)) (DC _ _ (pr2 x) (pr2 y))). - exact (total_category_BinCoproductIn1 x y (PC (pr1 x) (pr1 y)) (DC _ _ (pr2 x) (pr2 y))). - exact (total_category_BinCoproductIn2 x y (PC (pr1 x) (pr1 y)) (DC _ _ (pr2 x) (pr2 y))). - exact (total_category_isBinCoproduct x y (PC (pr1 x) (pr1 y)) (DC _ _ (pr2 x) (pr2 y))). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total.