Definition is_dispBinProduct_dispBinProduct {c d : C} (P : BinProduct C c d) {cc : D c} {dd : D d} (dP : dispBinProduct c d P cc dd) : is_dispBinProduct c d P cc dd (dispBinProductObject P dP) (dispBinProductPr1 P dP) (dispBinProductPr2 P dP). Proof. exact (pr2 dP). 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.