for C, D being terminal category holds C ~= D