Definition preserves_pullback_bindelta_pair_functor {C D₁ D₂ : category} {F : C ⟶ D₁} {G : C ⟶ D₂} (HF : preserves_pullback F) (HG : preserves_pullback G) : preserves_pullback (bindelta_pair_functor F G). Proof. intros w x y z f g π₁ π₂ p₁ p₂ H. apply isPullback_in_product_category. - exact (HF _ _ _ _ _ _ _ _ _ _ H). - exact (HG _ _ _ _ _ _ _ _ _ _ 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.