Proposition composition_preserves_chosen_equalizers_eq {C₁ C₂ C₃ : category} {F : C₁ ⟶ C₂} {G : C₂ ⟶ C₃} {BE₁ : Equalizers C₁} {BE₂ : Equalizers C₂} {BE₃ : Equalizers C₃} (HF : preserves_chosen_equalizers_eq F BE₁ BE₂) (HG : preserves_chosen_equalizers_eq G BE₂ BE₃) : preserves_chosen_equalizers_eq (F ∙ G) BE₁ BE₃. Proof. intros x y 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.