Lemma BinProduct_of_functors_commutes_law : is_nat_trans _ _ BinProduct_of_functors_commutes_data. Proof. intros c c' f. cbn. unfold BinProduct_of_functors_mor. etrans. 2: { apply pathsinv0, postcompWithBinProductArrow. } apply BinProductArrowUnique. - rewrite assoc'. etrans. { apply maponpaths. apply BinProductPr1Commutes. } etrans. { apply BinProductOfArrowsPr2. } apply idpath. - rewrite assoc'. etrans. { apply maponpaths. apply BinProductPr2Commutes. } etrans. { apply BinProductOfArrowsPr1. } 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.