Definition preserves_pullback_if_preserves_chosen {C₁ C₂ : category} (HC₁ : Pullbacks C₁) (F : C₁ ⟶ C₂) (HF : preserves_chosen_pullback HC₁ F) : preserves_pullback F. Proof. intros x y z pb f g π₁ π₂ p Hxy Hpb. apply (isPullback_z_iso _ _ (HF x y z f g) (functor_on_z_iso F (z_iso_from_Pullback_to_Pullback (HC₁ _ _ _ f g) (make_Pullback _ Hpb)))). - abstract (cbn ; rewrite <- !functor_comp ; apply maponpaths ; apply (PullbackArrow_PullbackPr1 (make_Pullback p Hpb))). - abstract (cbn ; rewrite <- !functor_comp ; apply maponpaths ; apply (PullbackArrow_PullbackPr2 (make_Pullback p Hpb))). 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.