Definition isBinProduct_eq_arrow {C : category} {x y z : C} {π₁ π₁' : z --> x} (p₁ : π₁ = π₁') {π₂ π₂' : z --> y} (p₂ : π₂ = π₂') (H : isBinProduct C x y z π₁ π₂) : isBinProduct C x y z π₁' π₂'. Proof. pose (P := make_BinProduct _ _ _ _ _ _ H). use make_isBinProduct. intros w f g. use iscontraprop1. - abstract (induction p₁, p₂ ; apply isapropifcontr ; apply H). - simple refine (_ ,, _ ,, _). + exact (BinProductArrow _ P f g). + abstract (induction p₁ ; exact (BinProductPr1Commutes _ _ _ P _ f g)). + abstract (induction p₂ ; exact (BinProductPr2Commutes _ _ _ P _ f g)). Defined.
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.