Lemma pb_LModule_Mor_law : LModule_Mor_laws M (T:=pbmT) (T':=pbmT') n. Proof. intros b. cbn. eapply pathscomp0; revgoals. - rewrite <-assoc. apply cancel_precomposition. apply LModule_Mor_σ. - repeat rewrite assoc. apply cancel_postcomposition. apply pathsinv0. apply nat_trans_ax. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Monads.Monads.