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. 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.
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.