Definition total_category_Binproducts_mediating_morphism (Ps : BinProducts C) (dPs : dispBinProducts Ps) {c d x : C} {cc : D c} {dd: D d} {xx : D x} {f : x --> c} (ff: xx -->[f] cc) {g : x --> d} (gg: xx -->[g] dd) : ∑ h : x --> BinProductObject C (Ps c d), xx -->[h] dispBinProductObject (Ps c d) (dPs c d cc dd). Proof. use tpair. - apply BinProductArrow; assumption. - apply dispBinProductArrow; assumption. 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.