Definition total_category_isCoproduct : isCoproduct _ _ _ total_category_Coproduct total_category_CoproductIn. Proof. intros w f. use iscontraprop1. - apply total_category_CoproductUnique. - simple refine (_ ,, _). + exact (total_category_CoproductArrow (pr2 w) (λ i, pr2 (f i))). + exact (total_category_CoproductInCommutes (pr2 w) (λ i, pr2 (f i))). 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.