:: deftheorem Def13 defines Concretization YELLOW18:def 13 :
for A being category
for b₂ being strict covariant Functor of A, Concretized A holds
( b₂ = Concretization A iff ( ( for a being Object of A holds b₂ . a = a ) & ( for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (b₂ . f) . [(idm a),[a,a]] = [f,[a,b]] ) ) );