Lemma BinProduct_assoc_is_inverse : is_inverse_in_precat BinProduct_assoc_mor BinProduct_assoc_invmor. Proof. use make_is_inverse_in_precat. - unfold BinProduct_assoc_mor, BinProduct_assoc_invmor. use BinProductArrowsEq. * now rewrite id_left, assoc', BinProductPr1Commutes, assoc, BinProductPr1Commutes, BinProductOfArrowsPr1, id_right. * now rewrite id_left, assoc', BinProductPr2Commutes, postcompWithBinProductArrow, id_right, BinProductOfArrowsPr2, <-precompWithBinProductArrow, <-(id_left (BinProductPr1 C Pbc)), <-(id_left (BinProductPr2 C Pbc)), <-BinProductArrowEta, id_right. - unfold BinProduct_assoc_mor, BinProduct_assoc_invmor. use BinProductArrowsEq. * now rewrite id_left, assoc', BinProductPr1Commutes, postcompWithBinProductArrow, id_right, BinProductOfArrowsPr1, <-precompWithBinProductArrow, <-(id_left (BinProductPr1 C Pab)), <-(id_left (BinProductPr2 C Pab)), <-BinProductArrowEta, id_right. * now rewrite id_left, assoc', BinProductPr2Commutes, assoc, BinProductPr2Commutes, BinProductOfArrowsPr2, id_right. 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.