for C1, C2 being category holds Functors (C1,C2) ~= C2 |^ C1