for C, D, D9 being Category
for T being Functor of C,D
for T9 being Functor of C,D9
for c being Object of C holds (Obj <:T,T9:>) . c = [((Obj T) . c),((Obj T9) . c)]