Lemma dispBinProductArrowUnique {c d : C} (P : BinProduct C c d) (cc : D c) (dd : D d) (dP : dispBinProduct c d P cc dd) {x : C} (xx : D x) (f : x --> c) (g : x --> d) (ff : xx -->[f] cc) (gg : xx -->[g] dd) (kk : xx -->[BinProductArrow _ P f g] dispBinProductObject P dP) : kk ;; dispBinProductPr1 P dP = transportb _ (BinProductPr1Commutes _ _ _ P _ f g) ff -> kk ;; dispBinProductPr2 P dP = transportb _ (BinProductPr2Commutes _ _ _ P _ f g) gg -> kk = dispBinProductArrow P dP ff gg. Proof. intros H1 H2. apply path_to_ctr; split; assumption. Qed.
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.