Definition preserves_binproduct_bindelta_pair_functor {C D₁ D₂ : category} {F : C ⟶ D₁} {G : C ⟶ D₂} (HF : preserves_binproduct F) (HG : preserves_binproduct G) : preserves_binproduct (bindelta_pair_functor F G). Proof. intros x y z π₁ π₂ H. apply isBinProduct_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.