for UN being Universe
for f, g being Morphism of (GroupCat UN) holds
( [g,f] in dom the Comp of (GroupCat UN) iff dom g = cod f )