Definition total_category_isBinCoproduct : isBinCoproduct _ _ _ total_category_BinCoproduct total_category_BinCoproductIn1 total_category_BinCoproductIn2. Proof. intros w f g. use iscontraprop1. - apply total_category_BinCoproductUnique. - simple refine (_ ,, _ ,, _). + exact (total_category_BinCoproductArrow (pr2 w) (pr2 f) (pr2 g)). + apply total_category_BinCoproductArrowIn1. + apply total_category_BinCoproductArrowIn2. 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.