Definition preserves_chosen_pullback {C₁ C₂ : category} (HC₁ : Pullbacks C₁) (F : C₁ ⟶ C₂) : UU. Proof. refine (∏ (x y z : C₁) (f : x --> z) (g : y --> z), @isPullback C₂ (F z) (F x) (F y) (F (PullbackObject (HC₁ _ _ _ f g))) (#F f) (#F g) (#F (PullbackPr1 (HC₁ _ _ _ f g))) (#F (PullbackPr2 (HC₁ _ _ _ f g))) _). abstract (rewrite <- !functor_comp ; apply maponpaths ; apply PullbackSqrCommutes). 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.