Iso VS equality in cartesian product of categories

Stream: mathlib4

[Nicolas Rolland]

We have a lemma for the cartesian product of categories, CategoryTheory.prod.etaIso, proving the isomorphism (X.1, X.2) ≅ X

I don't find any corresponding lemma for the equality.
Is there any deep reason for this ?

This product is not any universal product, characterized up to iso.
It is the product that we chose and built up, so we have

def prod.etaEq (X : C × D) : (X.1, X.2) = X := rfl

[Kevin Buzzard]

Equality of objects is not a well-behaved concept in category theory, is presumably why we don't have it

[Kevin Buzzard]

Like groups are "only defined up to isomorphism", categories are "only defined up to equivalence", and equality of objects is not preserved by equivalence. I can't imagine anyone objecting to you adding it though.

[Kim Morrison]

I suspect rather that here that statement, which is just about products and nothing about categories, already exists.