:: deftheorem defines GroupCat GRCAT_1:def 30 :
for UN being Universe holds GroupCat UN = CatStr(# (GroupObjects UN),(Morphs (GroupObjects UN)),(dom (GroupObjects UN)),(cod (GroupObjects UN)),(comp (GroupObjects UN)) #);