Corollary weak_equiv_preserves_chosen_binproducts {C D : category} {F : C ⟶ D} (Fw : is_weak_equiv F) (BP : BinProducts C) : preserves_chosen_binproduct BP F. Proof. intros x1 x2. use (weak_equiv_preserves_binproducts Fw). apply isBinProduct_BinProduct. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.WeakEquivalences.Core. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Preservation.