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. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.Monoids. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Terminal.