:: deftheorem Def5 defines dualizing-func YELLOW18:def 5 :
for A, B being category st A,B are_opposite holds
for b₃ being strict contravariant Functor of A,B holds
( b₃ = dualizing-func (A,B) iff ( ( for a being Object of A holds b₃ . a = a ) & ( for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds b₃ . f = f ) ) );