Lemma weak_equiv_preserves_binproducts_pr1 : weak_equiv_preserves_binproducts_map · # F (BinProductPr1 C BP) = g1. Proof. unfold weak_equiv_preserves_binproducts_map. rewrite assoc'. rewrite <- functor_comp. rewrite BinProductPr1Commutes. unfold f1; rewrite functor_on_fully_faithful_inv_hom. rewrite assoc. rewrite z_iso_after_z_iso_inv. apply id_left. 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.