:: deftheorem defines CohCat COH_SP:def 15 :
for X being set holds CohCat X = CatStr(# (CSp X),(MapsC X),(CDom X),(CCod X),(CComp X) #);