proposition: Lemma bincoprod_associator_inverses (c d e : C) : is_inverse_in_precat (bincoprod_associator_data c d e) (bincoprod_associatorinv_data c d e).
proof: Proof. split. + apply pathsinv0, BinCoproduct_endo_is_identity. * rewrite assoc. etrans. { apply cancel_postcomposition. apply BinCoproductIn1Commutes. } use BinCoproductArrowsEq. -- repeat rewrite assoc. etrans. { apply cancel_postcomposition. apply BinCoproductIn1Commutes. } rewrite id_left. etrans. { apply BinCoproductIn1Commutes. } apply idpath. -- repeat rewrite assoc. etrans. { apply cancel_postcomposition. apply BinCoproductIn2Commutes. } etrans. { rewrite assoc'. apply maponpaths. apply BinCoproductIn2Commutes. } apply BinCoproductOfArrowsIn1. * rewrite assoc. etrans. { apply cancel_postcomposition. apply BinCoproductIn2Commutes. } etrans. { rewrite assoc'. apply maponpaths. apply BinCoproductIn2Commutes. } rewrite BinCoproductOfArrowsIn2. apply id_left. + apply pathsinv0, BinCoproduct_endo_is_identity. * rewrite assoc. etrans. { apply cancel_postcomposition. apply BinCoproductIn1Commutes. } etrans. { rewrite assoc'. apply maponpaths. apply BinCoproductIn1Commutes. } rewrite BinCoproductOfArrowsIn1. apply id_left. * rewrite assoc. etrans. { apply cancel_postcomposition. apply BinCoproductIn2Commutes. } use BinCoproductArrowsEq. -- repeat rewrite assoc. etrans. { apply cancel_postcomposition. apply BinCoproductOfArrowsIn1. } etrans. { rewrite assoc'. apply maponpaths. apply BinCoproductIn1Commutes. } apply BinCoproductOfArrowsIn2. -- repeat rewrite assoc. etrans. { apply cancel_postcomposition. apply BinCoproductOfArrowsIn2. } rewrite id_left. etrans. { apply BinCoproductIn2Commutes. } apply idpath. 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