proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.Coequalizers UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Adjunctions.Core