Definition pr1_preserves_binproduct {C₁ C₂ : category} (HC₁ : BinProducts C₁) (HC₂ : BinProducts C₂) : preserves_binproduct (pr1_functor C₁ C₂). Proof. use preserves_binproduct_if_preserves_chosen. - apply binproducts_in_product_category. + exact HC₁. + exact HC₂. - intros x y. apply isBinProduct_BinProduct. 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.Isos. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Preservation.