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. 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.
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.