Lemma weak_equiv_reflect_binproducts_first_projection_commute : fg · π₁ = f1. Proof. unfold fg. refine (! homotinvweqweq (weq_from_fully_faithful Fw _ _) _ @ _). refine (_ @ homotinvweqweq (weq_from_fully_faithful Fw _ _) _). apply maponpaths. simpl. rewrite functor_comp. etrans. { apply maponpaths_2. apply (homotweqinvweq (weq_from_fully_faithful Fw _ _)). } exact (pr121 (Hp _ (#F f1) (#F f2))). 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.