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