for A being Category
for o, m being set holds [:(1Cat (o,m)),A:] ~= A