Proposition weak_equiv_preserves_binproducts {C D : category} {F : C ⟶ D} (Fw : is_weak_equiv F) : preserves_binproduct F. Proof. intros x1 x2 px π₁ π₂ Hyp. pose (BP := make_BinProduct _ _ _ _ _ _ Hyp). intros y g1 g2. use (factor_through_squash (isapropiscontr _) _ (eso_from_weak_equiv _ Fw y)). intros [x yi]. use iscontraprop1. - exact (weak_equiv_preserves_binproducts_unique Fw BP _ _ yi). - simple refine (_ ,, _ ,, _). + exact (weak_equiv_preserves_binproducts_map Fw BP g1 g2 yi). + apply (weak_equiv_preserves_binproducts_pr1 Fw BP). + apply (weak_equiv_preserves_binproducts_pr2 Fw BP). 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.