proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.ProductCategory