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