I suppose it's possible that, somewhere, we will care about judgemental equality of categories for non-pragmatic reasons, and that having these extra fields will cause trouble there.  But I'm dubious.

The reason that I added this field was so that I could define colimits as opposite limits; without it, the appropriate types don't unify.