Proposition preserves_binproduct_of_arrows {C₁ C₂ : category} {BC₁ : BinProducts C₁} {BC₂ : BinProducts C₂} {F : C₁ ⟶ C₂} (HF : preserves_binproduct F) {x₁ x₂ y₁ y₂ : C₁} (f : x₁ --> x₂) (g : y₁ --> y₂) : inv_from_z_iso (preserves_binproduct_to_z_iso F HF _ _) · #F(BinProductOfArrows _ (BC₁ _ _) (BC₁ _ _) f g) = BinProductOfArrows _ (BC₂ _ _) (BC₂ _ _) (#F f) (#F g) · inv_from_z_iso (preserves_binproduct_to_z_iso F HF _ _). Proof. cbn. pose (H₁ := preserves_binproduct_to_binproduct F HF (BC₁ x₁ y₁)). pose (H₂ := preserves_binproduct_to_binproduct F HF (BC₁ x₂ y₂)). use (BinProductArrowsEq _ _ _ (preserves_binproduct_to_binproduct F HF (BC₁ x₂ y₂))). - etrans. { unfold BinProductOfArrows. apply maponpaths_2. apply maponpaths. apply (preserves_binproduct_to_preserves_arrow F HF (BC₁ _ _) (BC₂ _ _)). } cbn. rewrite !assoc'. etrans. { do 2 apply maponpaths. apply (BinProductPr1Commutes _ _ _ H₂). } rewrite BinProductPr1Commutes. etrans. { rewrite functor_comp. rewrite !assoc. apply maponpaths_2. apply (BinProductPr1Commutes _ _ _ H₁). } refine (!_). etrans. { apply maponpaths. apply (BinProductPr1Commutes _ _ _ H₂). } rewrite BinProductOfArrowsPr1. apply idpath. - etrans. { unfold BinProductOfArrows. apply maponpaths_2. apply maponpaths. apply (preserves_binproduct_to_preserves_arrow F HF (BC₁ _ _) (BC₂ _ _)). } cbn. rewrite !assoc'. etrans. { do 2 apply maponpaths. apply (BinProductPr2Commutes _ _ _ H₂). } rewrite BinProductPr2Commutes. etrans. { rewrite functor_comp. rewrite !assoc. apply maponpaths_2. apply (BinProductPr2Commutes _ _ _ H₁). } refine (!_). etrans. { apply maponpaths. apply (BinProductPr2Commutes _ _ _ H₂). } rewrite BinProductOfArrowsPr2. apply idpath. 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.