Proposition weak_equiv_reflects_products {C D : category} {F : C ⟶ D} (Fw : fully_faithful F) : ∏ (c1 c2 p : C) (π₁ : C⟦p, c1⟧) (π₂ : C⟦p, c2⟧), isBinProduct _ (F c1) (F c2) (F p) (#F π₁) (#F π₂) → isBinProduct _ c1 c2 p π₁ π₂. Proof. intros. intros x f1 f2. use iscontraprop1. - apply (weak_equiv_reflect_binproducts_uvp_uniqueness Fw _ _ _ _ _ X). - apply (weak_equiv_reflect_binproducts_uvp_existence Fw _ _ _ _ _ X). 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.