for A being Category
for f being Morphism of A holds <|(cod f),?> is_naturally_transformable_to <|(dom f),?>