Lemma BinProduct_endo_is_identity (P : BinProduct _ a b) (k : BinProductObject _ P --> BinProductObject _ P) (H1 : k · BinProductPr1 _ P = BinProductPr1 _ P) (H2 : k · BinProductPr2 _ P = BinProductPr2 _ P) : identity _ = k. Proof. apply pathsinv0. eapply pathscomp0. apply BinProductArrowEta. apply pathsinv0. apply BinProductArrowUnique; apply pathsinv0. + rewrite id_left. exact H1. + rewrite id_left. exact H2. 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.