proposition: Lemma islunit_cat_comm {fM : C⟦M ⊗ M,M⟧} {fL : C⟦L ⊗ L,L⟧} (Hf : fM · i = (i ×× i) · fL) {gM : C ⟦TC,M⟧} {gL : C⟦TC,L⟧} (Hg : gM · i = gL) : islunit_cat fL gL → islunit_cat fM gM.
proof: Proof. unfold islunit_cat; intros H; apply Hi. rewrite <-!assoc. etrans; [ do 2 apply maponpaths; apply Hf |]. rewrite identity_comm, <-H, postcompWithBinProductArrow, !assoc. apply cancel_postcomposition. rewrite !postcompWithBinProductArrow, <-assoc, Hg, !id_left. apply pathsinv0, BinProductArrowUnique. - rewrite <- assoc, BinProductPr1Commutes, assoc. now apply cancel_postcomposition, TerminalArrowUnique. - now rewrite <- assoc, BinProductPr2Commutes, id_right. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.Algebra.Monoids UniMath.OrderTheory.Lattice.Lattice UniMath.OrderTheory.Lattice.Bounded UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Terminal