Lemma postcompWithBinProductArrow {c d : C} (Pcd : BinProduct c d) {a b : C} (Pab : BinProduct a b) (f : a --> c) (g : b --> d) {x : C} (k : x --> a) (h : x --> b) : BinProductArrow Pab k h · BinProductOfArrows Pcd Pab f g = BinProductArrow Pcd (k · f) (h · g). Proof. apply BinProductArrowUnique. - rewrite <- assoc, BinProductOfArrowsPr1. rewrite assoc, BinProductPr1Commutes. apply idpath. - rewrite <- assoc, BinProductOfArrowsPr2. rewrite assoc, BinProductPr2Commutes. 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.