for C being Category holds 1Cat (C,[[C,C],(id C)]) is Categorial