proposition: Lemma weak_equiv_preserves_binproducts_unique : isaprop (∑ fg : D⟦y, F BP⟧, fg · # F (BinProductPr1 C BP) = g1 × fg · # F (BinProductPr2 C BP) = g2).
proof: Proof. use invproofirrelevance. intros φ₁ φ₂. use subtypePath. { intro. apply isapropdirprod ; apply homset_property. } use (cancel_z_iso' yi). refine (! homotweqinvweq (weq_from_fully_faithful (ff_from_weak_equiv _ Fw) _ _) _ @ _). refine (_ @ homotweqinvweq (weq_from_fully_faithful (ff_from_weak_equiv _ Fw) _ _) _). apply maponpaths. use BinProductArrowsEq. - refine (! homotinvweqweq (weq_from_fully_faithful (ff_from_weak_equiv _ Fw) _ _) _ @ _). refine (_ @ homotinvweqweq (weq_from_fully_faithful (ff_from_weak_equiv _ Fw) _ _) _). apply maponpaths. simpl. rewrite ! functor_comp. etrans. { apply maponpaths_2. apply (homotweqinvweq (weq_from_fully_faithful (ff_from_weak_equiv _ Fw) _ _)). } refine (! _). etrans. { apply maponpaths_2. apply (homotweqinvweq (weq_from_fully_faithful (ff_from_weak_equiv _ Fw) _ _)). } rewrite ! assoc'. apply maponpaths. exact (pr12 φ₂ @ ! pr12 φ₁). - refine (! homotinvweqweq (weq_from_fully_faithful (ff_from_weak_equiv _ Fw) _ _) _ @ _). refine (_ @ homotinvweqweq (weq_from_fully_faithful (ff_from_weak_equiv _ Fw) _ _) _). apply maponpaths. simpl. rewrite ! functor_comp. etrans. { apply maponpaths_2. apply (homotweqinvweq (weq_from_fully_faithful (ff_from_weak_equiv _ Fw) _ _)). } refine (! _). etrans. { apply maponpaths_2. apply (homotweqinvweq (weq_from_fully_faithful (ff_from_weak_equiv _ Fw) _ _)). } rewrite ! assoc'. apply maponpaths. exact (pr22 φ₂ @ ! pr22 φ₁). 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