Definition disp_isBinCoproduct {x y : C} {xx : D x} {yy : D y} (p : BinCoproduct x y) (pp : D p) (ιι₁ : xx -->[ BinCoproductIn1 p ] pp) (ιι₂ : yy -->[ BinCoproductIn2 p ] pp) : UU := ∏ (w : C) (ww : D w) (f : x --> w) (ff : xx -->[ f ] ww) (g : y --> w) (gg : yy -->[ g ] ww), ∃! (hh : pp -->[ BinCoproductArrow p f g ] ww), (transportf (λ z, _ -->[ z ] _) (BinCoproductIn1Commutes _ _ _ p _ f g) (ιι₁ ;; hh) = ff) × (transportf (λ z, _ -->[ z ] _) (BinCoproductIn2Commutes _ _ _ p _ f g) (ιι₂ ;; hh) = gg).
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.