Definition preserves_bincoproduct_if_preserves_chosen {C₁ C₂ : category} (HC₁ : BinCoproducts C₁) (F : C₁ ⟶ C₂) (HF : preserves_chosen_bincoproduct HC₁ F) : preserves_bincoproduct F. Proof. intros x y z ι₁ ι₂ Hxy. use (isBinCoproduct_eq_arrow _ _ (z_iso_to_isBinCoproduct _ (make_BinCoproduct _ _ _ _ _ _ (HF x y)) (functor_on_z_iso F (z_iso_from_BinCoproduct_to_BinCoproduct _ (make_BinCoproduct _ _ _ _ _ _ Hxy) (HC₁ x y))))) ; cbn. - abstract (rewrite <- functor_comp ; apply maponpaths ; apply BinCoproductIn1Commutes). - abstract (rewrite <- functor_comp ; apply maponpaths ; apply BinCoproductIn2Commutes). 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.