:: deftheorem Def14 defines SliceContraFunctor CAT_5:def 14 :
for C being Category
for f being Morphism of C
for b₃ being Functor of (cod f) -SliceCat C,(dom f) -SliceCat C holds
( b₃ = SliceContraFunctor f iff for m being Morphism of ((cod f) -SliceCat C) holds b₃ . m = [[((m `11) (*) f),((m `12) (*) f)],(m `2)] );