Definition pr2_preserves_pullback {C₁ C₂ : category} (HC₁ : Pullbacks C₁) (HC₂ : Pullbacks C₂) : preserves_pullback (pr2_functor C₁ C₂). Proof. use preserves_pullback_if_preserves_chosen. - apply pullbacks_in_product_category. + exact HC₁. + exact HC₂. - intros x y z f g. apply isPullback_Pullback. 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.