Lemma preserves_bincoproduct_to_preserves_arrow {Y : C₁} (f : X --> Y) (f' : X' --> Y) : inv_from_z_iso preserves_bincoproduct_to_z_iso · #F (BinCoproductArrow BP f f') = BinCoproductArrow BP' (#F f) (#F f'). Proof. apply BinCoproductArrowsEq. - cbn. unfold from_BinCoproduct_to_BinCoproduct. rewrite !assoc. rewrite !BinCoproductIn1Commutes. cbn. rewrite <- functor_comp. apply maponpaths. apply BinCoproductIn1Commutes. - cbn. unfold from_BinCoproduct_to_BinCoproduct. rewrite !assoc. rewrite !BinCoproductIn2Commutes. cbn. rewrite <- functor_comp. apply maponpaths. apply BinCoproductIn2Commutes. 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.