:: deftheorem Def12 defines -SliceCat CAT_5:def 12 :
for C being Category
for o being Object of C
for b₃ being strict with_triple-like_morphisms Category holds
( b₃ = o -SliceCat C iff ( the carrier of b₃ = o Hom & ( for a, b being Element of o Hom
for f being Morphism of C st dom f = cod a & f (*) a = b holds
[[a,b],f] is Morphism of b₃ ) & ( for m being Morphism of b₃ ex a, b being Element of o Hom ex f being Morphism of C st
( m = [[a,b],f] & dom f = cod a & f (*) a = b ) ) & ( for m1, m2 being Morphism of b₃
for a1, a2, a3 being Element of o Hom
for f1, f2 being Morphism of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 (*) m1 = [[a1,a3],(f2 (*) f1)] ) ) );