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. 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.
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.