:: deftheorem Def11 defines Upsilon CATALG_1:def 11 :
for C1, C2 being Category
for F being Functor of C1,C2
for b₄ being Function of the carrier of (CatSign the carrier of C1), the carrier of (CatSign the carrier of C2) holds
( b₄ = Upsilon F iff for s being SortSymbol of (CatSign the carrier of C1) holds b₄ . s = [0,((Obj F) * (s `2))] );