Lemma bincoprod_antidistributor_commutes_with_associativity_of_coproduct (c d e : C) : #(bincoproduct_functor BCPD) (catbinprodmor (bincoprod_antidistributor c d) (identity (F e))) · bincoprod_antidistributor (BCPC c d) e · #F (bincoprod_associator_data BCPC c d e) = bincoprod_associator_data BCPD (F c) (F d) (F e) · #(bincoproduct_functor BCPD) (catbinprodmor (identity (F c)) (bincoprod_antidistributor d e)) · bincoprod_antidistributor c (BCPC d e). Proof. etrans. { apply cancel_postcomposition. apply precompWithBinCoproductArrow. } etrans. { apply postcompWithBinCoproductArrow. } etrans. 2: { rewrite assoc'. apply maponpaths. apply pathsinv0, precompWithBinCoproductArrow. } etrans. 2: { apply pathsinv0, postcompWithBinCoproductArrow. } apply maponpaths_12. - etrans. 2: { apply pathsinv0, precompWithBinCoproductArrow. } etrans. { rewrite assoc'. apply maponpaths. etrans. { apply pathsinv0, functor_comp. } apply maponpaths. apply BinCoproductIn1Commutes. } etrans. { cbn. apply postcompWithBinCoproductArrow. } apply maponpaths_12. + cbn. do 2 rewrite id_left. etrans. { apply pathsinv0, functor_comp. } apply maponpaths. rewrite BinCoproductOfArrowsIn1. apply id_left. + cbn. etrans. { apply pathsinv0, functor_comp. } etrans. { apply maponpaths. apply BinCoproductOfArrowsIn2. } rewrite assoc. etrans. 2: { apply cancel_postcomposition. apply pathsinv0, BinCoproductIn1Commutes. } apply functor_comp. - etrans. { cbn. rewrite id_left. apply pathsinv0, functor_comp. } etrans. 2: { rewrite assoc'. apply maponpaths. apply pathsinv0, BinCoproductIn2Commutes. } cbn. rewrite assoc. etrans. 2: { apply cancel_postcomposition. apply pathsinv0, BinCoproductIn2Commutes. } etrans. { apply maponpaths. apply BinCoproductIn2Commutes. } apply functor_comp. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Limits.Zero. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.ProductCategory.