Definition disp_isCoproduct {d : I → C} (dd : ∏ (i : I), D (d i)) (p : Coproduct I C d) (pp : D p) (ππ : ∏ (i : I), dd i -->[ CoproductIn _ _ p i ] pp) : UU := ∏ (w : C) (ww : D w) (f : ∏ (i : I), d i --> w) (ff : ∏ (i : I), dd i -->[ f i ] ww), ∃! (hh : pp -->[ CoproductArrow _ _ p f ] ww), ∏ (i : I), transportf (λ z, _ -->[ z ] _) (CoproductInCommutes _ _ _ p _ f i) (ππ i ;; hh) = ff i.
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.