Definition preserves_binproduct_if_preserves_chosen (HF : preserves_chosen_binproduct) : preserves_binproduct. Proof. intros x y z π₁ π₂ Hxy. use (isBinProduct_eq_arrow _ _ (pr2 (iso_to_BinProduct _ (make_BinProduct _ _ _ _ _ _ (HF x y)) (z_iso_to_iso (functor_on_z_iso F (iso_between_BinProduct (make_BinProduct _ _ _ _ _ _ Hxy) (HC₁ x y))))))) ; cbn. - abstract (rewrite <- functor_comp ; rewrite BinProductPr1Commutes ; apply idpath). - abstract (rewrite <- functor_comp ; rewrite BinProductPr2Commutes ; apply idpath). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Limits.Pushouts. Require Import UniMath.CategoryTheory.Adjunctions.Core.