Proposition BinProductOfArrows_swap {x₁ x₂ : C} {y₁ y₂ : C} (f : x₁ --> x₂) (g : y₁ --> y₂) : BinProductOfArrows C (prodC _ _) (prodC _ _) f g · prod_swap x₂ y₂ = prod_swap x₁ y₁ · BinProductOfArrows C _ _ g f. Proof. use BinProductArrowsEq. - unfold prod_swap. rewrite !assoc'. rewrite BinProductPr1Commutes. rewrite BinProductOfArrowsPr2. rewrite BinProductOfArrowsPr1. rewrite !assoc. rewrite BinProductPr1Commutes. apply idpath. - unfold prod_swap. rewrite !assoc'. rewrite BinProductPr2Commutes. rewrite BinProductOfArrowsPr2. rewrite BinProductOfArrowsPr1. rewrite !assoc. rewrite 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.