:: deftheorem defines comma COMMACAT:def 5 :
for C, D, E being Category
for F being Functor of C,E
for G being Functor of D,E st ex c1 being Object of C ex d1 being Object of D ex f1 being Morphism of E st f1 in Hom ((F . c1),(G . d1)) holds
for b₆ being strict Category holds
( b₆ = F comma G iff ( the carrier of b₆ = commaObjs (F,G) & the carrier' of b₆ = commaMorphs (F,G) & ( for k being Element of commaMorphs (F,G) holds the Source of b₆ . k = k `11 ) & ( for k being Element of commaMorphs (F,G) holds the Target of b<sub>6</sub> . k = k `12 ) & the Comp of b₆ = commaComp (F,G) ) );