Proposition composition_preserves_chosen_pullbacks_eq {C₁ C₂ C₃ : category} {F : C₁ ⟶ C₂} {G : C₂ ⟶ C₃} {P₁ : Pullbacks C₁} {P₂ : Pullbacks C₂} {P₃ : Pullbacks C₃} (HF : preserves_chosen_pullbacks_eq F P₁ P₂) (HG : preserves_chosen_pullbacks_eq G P₂ P₃) : preserves_chosen_pullbacks_eq (F ∙ G) P₁ P₃. Proof. intros x y z f g. use (factor_through_squash _ _ (HF _ _ _ f g)). { apply propproperty. } intros HFxy. use (factor_through_squash _ _ (HG _ _ _ (#F f) (#F g))). { apply propproperty. } intros HGxy. apply hinhpr. cbn in *. rewrite HFxy. now rewrite HGxy. Qed.
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.