for B, C being Category
for c being Object of C
for b being Object of B holds (Obj (B --> c)) . b = c