for C being Category
for E being Subcategory of C holds id E is Functor of E,C