:: deftheorem defines LModCat MODCAT_1:def 15 :
for UN being Universe
for R being Ring holds LModCat (UN,R) = CatStr(# (LModObjects (UN,R)),(Morphs (LModObjects (UN,R))),(dom (LModObjects (UN,R))),(cod (LModObjects (UN,R))),(comp (LModObjects (UN,R))) #);