Corollary weak_equiv_preserves_binproducts_eq {C D : category} {F : C ⟶ D} (Fw : is_weak_equiv F) (Duniv : is_univalent D) (BP₁ : BinProducts C) (BP₂ : BinProducts D) : preserves_chosen_binproducts_eq F BP₁ BP₂. Proof. intros x y. apply hinhpr. apply Duniv. set (Fp := weak_equiv_preserves_binproducts Fw). set (p := make_BinProduct _ _ _ _ _ _ (Fp x y (BP₁ x y) _ _ (pr2 (BP₁ x y)))). exact (iso_between_BinProduct p (BP₂ (F x) (F y))). 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.