Lemma BinProduct_of_functors_commutes_is_inverse (c: C) : is_inverse_in_precat (BinProduct_of_functors_commutes_data c) (BinProduct_of_functors_commutes_invdata c). Proof. split. - apply BinProductArrowsEq. + rewrite assoc'. etrans. { apply maponpaths. apply BinProductPr1Commutes. } etrans. { apply BinProductPr2Commutes. } apply pathsinv0, id_left. + rewrite assoc'. etrans. { apply maponpaths. apply BinProductPr2Commutes. } etrans. { apply BinProductPr1Commutes. } apply pathsinv0, id_left. - apply BinProductArrowsEq. + rewrite assoc'. etrans. { apply maponpaths. apply BinProductPr1Commutes. } etrans. { apply BinProductPr2Commutes. } apply pathsinv0, id_left. + rewrite assoc'. etrans. { apply maponpaths. apply BinProductPr2Commutes. } etrans. { apply BinProductPr1Commutes. } apply pathsinv0, id_left. 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.