proposition: Proposition composition_preserves_chosen_binproducts_eq {C₁ C₂ C₃ : category} {F : C₁ ⟶ C₂} {G : C₂ ⟶ C₃} {BP₁ : BinProducts C₁} {BP₂ : BinProducts C₂} {BP₃ : BinProducts C₃} (HF : preserves_chosen_binproducts_eq F BP₁ BP₂) (HG : preserves_chosen_binproducts_eq G BP₂ BP₃) : preserves_chosen_binproducts_eq (F ∙ G) BP₁ BP₃.
proof: Proof. intros x y. use (factor_through_squash _ _ (HF x y)). { apply propproperty. } intros HFxy. use (factor_through_squash _ _ (HG (F x) (F y))). { apply propproperty. } intros HGxy. apply hinhpr. cbn in *. rewrite HFxy. now rewrite HGxy. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.Coequalizers UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Adjunctions.Core