proposition: Lemma 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: Proof. intros. intros x f1 f2. use iscontraprop1. - apply (fg_unique Fw _ _ _ _ _ X). - simple refine (_ ,, _ ,, _). + exact (fg Fw _ _ _ _ _ X _ f1 f2). + apply fg_pr1. + apply fg_pr2. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Preservation UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.catiso UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.PrecompEquivalence