Definition weak_equiv_preserves_binproducts_map : D⟦y, F BP⟧ := inv_from_z_iso yi · #F (BinProductArrow _ BP f1 f2).
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.