proposition: Lemma LModule_same_func_Mor_is_inverse : is_inverse_in_precat (C := category_LModule R C) (LModule_same_func_Mor hm m1_law m2_law) (LModule_same_func_Mor (fun c => ! (hm c)) m2_law m1_law).
proof: Proof. use make_is_inverse_in_precat. - apply LModule_Mor_equiv. apply (id_left (C := [B, C])). - apply LModule_Mor_equiv. apply (id_right (C := [B, C])). Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Monads.Monads