Definition preserves_binproduct_chosen_to_chosen {C₁ C₂ : category} (P₁ : BinProducts C₁) (P₂ : BinProducts C₂) (F : C₁ ⟶ C₂) (HF : ∏ (x y : C₁), is_z_isomorphism (BinProductArrow _ (P₂ (F x) (F y)) (#F (BinProductPr1 _ (P₁ x y))) (#F (BinProductPr2 _ (P₁ x y))))) : preserves_binproduct F. Proof. use (preserves_binproduct_if_preserves_chosen P₁). intros x y. use (isBinProduct_z_iso (isBinProduct_BinProduct _ (P₂ (F x) (F y)))). - exact (_ ,, HF x y). - abstract (cbn ; rewrite BinProductPr1Commutes ; apply idpath). - abstract (cbn ; rewrite BinProductPr2Commutes ; apply idpath). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Limits.Pushouts. Require Import UniMath.CategoryTheory.Adjunctions.Core.