Lemma BinProductArrowsEq (c d : C) (P : BinProduct c d) (x : C) (k1 k2 : x --> BinProductObject P) : k1 · BinProductPr1 P = k2 · BinProductPr1 P -> k1 · BinProductPr2 P = k2 · BinProductPr2 P -> k1 = k2. Proof. intros H1 H2. set (p1 := k1 · BinProductPr1 P). set (p2 := k1 · BinProductPr2 P). rewrite (BinProductArrowUnique _ _ P _ p1 p2 k1). apply pathsinv0. apply BinProductArrowUnique. unfold p1. apply pathsinv0. apply H1. unfold p2. apply pathsinv0. apply H2. apply idpath. apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Zero. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.Combinatorics.StandardFiniteSets. Section BinProductFromIso. End BinProductFromIso. Section BinProductsFromProducts. End BinProductsFromProducts. Section ProductsFromBinProducts. End ProductsFromBinProducts.