:: deftheorem defines Switch CAT_4:def 15 :
for C being Cartesian_category
for a, b being Object of C holds Switch (a,b) = <:(pr2 (a,b)),(pr1 (a,b)):>;