Definition preserves_bincoproduct_bindelta_pair_functor {C D₁ D₂ : category} {F : C ⟶ D₁} {G : C ⟶ D₂} (HF : preserves_bincoproduct F) (HG : preserves_bincoproduct G) : preserves_bincoproduct (bindelta_pair_functor F G). Proof. intros x y z π₁ π₂ H. apply isBinCoproduct_in_product_category. - apply HF. apply H. - apply HG. apply H. 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.Isos. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Preservation.