Lemma preserves_binproduct_to_preserves_arrow {Y : C₁} (f : C₁⟦Y, X⟧) (f' : C₁⟦Y, X'⟧) : #F (BinProductArrow _ BP f f') = BinProductArrow _ BP' (#F f) (#F f') · inv_from_z_iso preserves_binproduct_to_z_iso. Proof. apply z_iso_inv_on_left. apply BinProductArrowsEq. - refine (!_ @ maponpaths _ (z_iso_inv_on_right _ _ _ _ _ _ preserves_binproduct_to_preserves_pr1)). refine (assoc _ _ _ @ _). refine (maponpaths (λ x, x · _) (assoc' _ _ _) @ _). refine (maponpaths (λ x, _ · x · _) (z_iso_inv_after_z_iso _) @ _). refine (maponpaths (λ x, x · _) (id_right _) @ _). refine (!functor_comp _ _ _ @ _). refine (maponpaths (λ x, #F x) (BinProductPr1Commutes _ _ _ _ _ _ _) @ !_). exact (BinProductPr1Commutes _ _ _ _ _ _ _). - refine (!_ @ maponpaths _ (z_iso_inv_on_right _ _ _ _ _ _ preserves_binproduct_to_preserves_pr2)). refine (assoc _ _ _ @ _). refine (maponpaths (λ x, x · _) (assoc' _ _ _) @ _). refine (maponpaths (λ x, _ · x · _) (z_iso_inv_after_z_iso _) @ _). refine (maponpaths (λ x, x · _) (id_right _) @ _). refine (!functor_comp _ _ _ @ _). refine (maponpaths (λ x, #F x) (BinProductPr2Commutes _ _ _ _ _ _ _) @ !_). exact (BinProductPr2Commutes _ _ _ _ _ _ _). Qed.
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.