Definition LModule_same_func_Mor {m1 m2 : R ∙ F ⟹ F } (hm : ∏ c, m1 c = m2 c) (m1_law : LModule_laws _ (F ,, m1)) (m2_law : LModule_laws _ (F ,, m2)) (M1 : LModule _ _ := _ ,, m1_law) (M2 : LModule _ _ := _ ,, m2_law) : LModule_Mor R M1 M2 := _ ,, LModule_same_func_Mor_laws hm .
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.